1 /-
2 Copyright (c) 2018 Kenny Lau. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Kenny Lau, Mario Carneiro, Johan Commelin
5 -/
6 import tactic.ring data.quot data.equiv.algebra ring_theory.ideal_operations group_theory.submonoid
src └─────────┘ └───────┘ └────────────────┘ └──────────────────────────┘ └────────────────────┘
7
8 universes u v
9
10 namespace localization
11 variables (α : Type u) [comm_ring α] (S : set α) [is_submonoid S]
12
13 def r (x y : α × S) : Prop :=
14 ∃ t ∈ S, ((x.2 : α) * y.1 - y.2 * x.1) * t = 0
15
16 local infix ≈ := r α S
17
18 section
19 variables {α S}
20 theorem r_of_eq {a₀ a₁ : α × S} (h : (a₀.2 : α) * a₁.1 = a₁.2 * a₀.1) : a₀ ≈ a₁ :=
21 ⟨1, is_submonoid.one_mem S, by rw [h, sub_self, mul_one]⟩
id ┴
src └──┘ └┘ └┘ ┴┴
typ └──┘ └┘ └┘ ┴┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ┴┴
22 end
23
24 theorem refl (x : α × S) : x ≈ x := r_of_eq rfl
id ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └─┘
src ┴ ┴ └─────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └─┘
25
26 theorem symm (x y : α × S) : x ≈ y → y ≈ x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
27 λ ⟨t, hts, ht⟩, ⟨t, hts, by rw [← neg_sub, ← neg_mul_eq_neg_mul, ht, neg_zero]⟩
id ┴┴ └─┘ └─────┘ └────────────────┘ └┘ └──────┘
src └────┘└─────┘└──┘└────────────────┘└┘ └┘└──────┘┴
typ ┴┴ └─┘ └────┘└─────┘└──┘└────────────────┘└┘└┘└┘└──────┘┴
doc └────┘ └──┘ └┘ └┘ ┴
txt └────┘ └──┘ └┘ └┘ ┴
par └────┘ └──┘ └┘ └┘ ┴
pid └──┘ └──┘ └┘ └┘ ┴
st └────────────┘└────────────────────┘└──┘└────────┘┴
28
29 theorem trans : ∀ (x y z : α × S), x ≈ y → y ≈ z → x ≈ z :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
30 λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨r₃, s₃, hs₃⟩ ⟨t, hts, ht⟩ ⟨t', hts', ht'⟩,
31 ⟨s₂ * t' * t, is_submonoid.mul_mem (is_submonoid.mul_mem hs₂ hts') hts,
id └──────────────────┘ └──────────────────┘
src └──────────────────┘ └──────────────────┘
typ └──────────────────┘ └──────────────────┘
32 calc (s₁ * r₃ - s₃ * r₁) * (s₂ * t' * t) =
33 t' * s₃ * ((s₁ * r₂ - s₂ * r₁) * t) + t * s₁ * ((s₂ * r₃ - s₃ * r₂) * t') :
34 by simp [mul_left_comm, mul_add, mul_comm]
src └────┘ └┘ └┘ └─
typ └────┘ └┘ └┘ └─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
35 ... = 0 : by simp only [subtype.coe_mk] at ht ht'; rw [ht, ht']; simp⟩
id └┘
src ───┘ └─────────┘ └─────────┘ └──┘ └┘ ┴ └──┘
typ ───┘ └─────────┘ └─────────┘ └──┘ └┘ └┘┴ └──┘
doc ───┘ └─────────┘ └─────────┘ └──┘ └┘ ┴ └──┘
txt ───┘ └─────────┘ └─────────┘ └──┘ └┘ ┴ └──┘
par ───┘ └─────────┘ └─────────┘ └──┘ └┘ ┴ └──┘
pid ───┘ ┴└──┘└┘ ┴┴└───────┘ └┘ └┘ ┴
st └┘┴└────┘
36
37 instance : setoid (α × S) :=
id └────┘ ┴ ┴ ┴
src └────┘ ┴
typ └────┘ ┴ ┴ ┴
38 ⟨r α S, refl α S, symm α S, trans α S⟩
id ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴
src ┴ └──┘ └──┘ └───┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴
39
40 end localization
41
42 /-- The localization of a ring at a submonoid:
43 the elements of the submonoid become invertible in the localization.-/
44 def localization (α : Type u) [comm_ring α] (S : set α) [is_submonoid S] :=
id └───────┘ ┴ └─┘ ┴ └──────────┘ ┴
src └───────┘ └─┘ └──────────┘
typ └───────┘ ┴ └─┘ ┴ └──────────┘ ┴
doc └──────────┘
45 quotient $ localization.setoid α S
id └──────┘ └─────────────────┘ ┴ ┴
src └──────┘ └─────────────────┘
typ └──────┘ └─────────────────┘ ┴ ┴
46
47 namespace localization
48 variables (α : Type u) [comm_ring α] (S : set α) [is_submonoid S]
id └───────┘ └─┘ └──────────┘
src └───────┘ └─┘ └──────────┘
typ └───────┘ └─┘ └──────────┘
doc └──────────┘
49
50 instance : has_add (localization α S) :=
51 ⟨quotient.lift₂
52 (λ x y : α × S, (⟦⟨x.2 * y.1 + y.2 * x.1, x.2 * y.2⟩⟧ : localization α S)) $
53 λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨r₃, s₃, hs₃⟩ ⟨r₄, s₄, hs₄⟩ ⟨t₅, hts₅, ht₅⟩ ⟨t₆, hts₆, ht₆⟩,
54 quotient.sound ⟨t₆ * t₅, is_submonoid.mul_mem hts₆ hts₅,
55 calc (s₁ * s₂ * (s₃ * r₄ + s₄ * r₃) - s₃ * s₄ * (s₁ * r₂ + s₂ * r₁)) * (t₆ * t₅) =
56 s₁ * s₃ * ((s₂ * r₄ - s₄ * r₂) * t₆) * t₅ + s₂ * s₄ * ((s₁ * r₃ - s₃ * r₁) * t₅) * t₆ : by ring
src └────
typ └────
doc └────
txt └────
par └────
pid └
57 ... = 0 : by simp only [subtype.coe_mk] at ht₅ ht₆; rw [ht₆, ht₅]; simp⟩⟩
src ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
typ ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
doc ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
txt ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
par ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
pid ─────┘ ┴└──┘└┘ ┴┴└────────┘ └┘ └┘ ┴
58
59 instance : has_neg (localization α S) :=
60 ⟨quotient.lift (λ x : α × S, (⟦⟨-x.1, x.2⟩⟧ : localization α S)) $
61 λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨t, hts, ht⟩,
62 quotient.sound ⟨t, hts,
63 calc (s₁ * -r₂ - s₂ * -r₁) * t = -((s₁ * r₂ - s₂ * r₁) * t) : by ring
src └────
typ └────
doc └────
txt └────
par └────
pid └
64 ... = 0 : by simp only [subtype.coe_mk] at ht; rw ht; simp⟩⟩
src ─────┘ └─────────┘ └─────┘ └─┘ └──┘
typ ─────┘ └─────────┘ └─────┘ └─┘ └──┘
doc ─────┘ └─────────┘ └─────┘ └─┘ └──┘
txt ─────┘ └─────────┘ └─────┘ └─┘ └──┘
par ─────┘ └─────────┘ └─────┘ └─┘ └──┘
pid ─────┘ ┴└──┘└┘ ┴┴└───┘ ┴
65
66 instance : has_mul (localization α S) :=
67 ⟨quotient.lift₂
68 (λ x y : α × S, (⟦⟨x.1 * y.1, x.2 * y.2⟩⟧ : localization α S)) $
69 λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨r₃, s₃, hs₃⟩ ⟨r₄, s₄, hs₄⟩ ⟨t₅, hts₅, ht₅⟩ ⟨t₆, hts₆, ht₆⟩,
70 quotient.sound ⟨t₆ * t₅, is_submonoid.mul_mem hts₆ hts₅,
71 calc ((s₁ * s₂) * (r₃ * r₄) - (s₃ * s₄) * (r₁ * r₂)) * (t₆ * t₅) =
72 t₆ * ((s₁ * r₃ - s₃ * r₁) * t₅) * r₂ * s₄ + t₅ * ((s₂ * r₄ - s₄ * r₂) * t₆) * r₃ * s₁ :
73 by simp [mul_left_comm, mul_add, mul_comm]
src └────┘ └┘ └┘ └─
typ └────┘ └┘ └┘ └─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
74 ... = 0 : by simp only [subtype.coe_mk] at ht₅ ht₆; rw [ht₅, ht₆]; simp⟩⟩
src ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
typ ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
doc ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
txt ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
par ─────┘ └─────────┘ └──────────┘ └──┘ └┘ ┴ └──┘
pid ─────┘ ┴└──┘└┘ ┴┴└────────┘ └┘ └┘ ┴
75
76 variables {α S}
77
78 def mk (r : α) (s : S) : localization α S := ⟦(r, s)⟧
id ┴ ┴ └──────────┘ ┴ ┴ ┴┴┴ ┴ ┴
src └──────────┘ ┴┴ ┴
typ ┴ ┴ └──────────┘ ┴ ┴ ┴┴┴ ┴ ┴
doc └──────────┘
79
80 /-- The natural map from the ring to the localization.-/
81 def of (r : α) : localization α S := mk r 1
id ┴ └──────────┘ ┴ ┴ └┘ ┴
src └──────────┘ └┘
typ ┴ └──────────┘ ┴ ┴ └┘ ┴
doc └──────────┘
82
83 instance : comm_ring (localization α S) :=
84 by refine
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
85 { add := has_add.add,
src └─────────────────┘ └─
typ └─────────────────┘ └─
doc └─────────────────┘ └─
txt └─────────────────┘ └─
par └─────────────────┘ └─
pid └─────────────────┘ └─
86 add_assoc := λ m n k, quotient.induction_on₃ m n k _,
src ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
typ ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
doc ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
txt ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
par ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
pid ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
87 zero := of 0,
src ───────────────────┘ └───
typ ───────────────────┘ └───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
88 zero_add := quotient.ind _,
src ───────────────────┘ └───
typ ───────────────────┘ └───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
89 add_zero := quotient.ind _,
src ───────────────────┘ └───
typ ───────────────────┘ └───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
90 neg := has_neg.neg,
src ───────────────────┘ └─
typ ───────────────────┘ └─
doc ───────────────────┘ └─
txt ───────────────────┘ └─
par ───────────────────┘ └─
pid ───────────────────┘ └─
91 add_left_neg := quotient.ind _,
src ───────────────────┘ └───
typ ───────────────────┘ └───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
92 add_comm := quotient.ind₂ _,
src ───────────────────┘ └───
typ ───────────────────┘ └───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
93 mul := has_mul.mul,
src ───────────────────┘ └─
typ ───────────────────┘ └─
doc ───────────────────┘ └─
txt ───────────────────┘ └─
par ───────────────────┘ └─
pid ───────────────────┘ └─
94 mul_assoc := λ m n k, quotient.induction_on₃ m n k _,
src ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
typ ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
doc ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
txt ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
par ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
pid ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
95 one := of 1,
src ───────────────────┘ └───
typ ───────────────────┘ └───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
96 one_mul := quotient.ind _,
src ───────────────────┘ └───
typ ───────────────────┘ └───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
97 mul_one := quotient.ind _,
src ───────────────────┘ └───
typ ───────────────────┘ └───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
98 left_distrib := λ m n k, quotient.induction_on₃ m n k _,
src ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
typ ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
doc ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
txt ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
par ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
pid ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
99 right_distrib := λ m n k, quotient.induction_on₃ m n k _,
src ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
typ ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
doc ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
txt ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
par ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
pid ───────────────────┘ └──────┘ ┴ ┴ ┴ └───
100 mul_comm := quotient.ind₂ _ };
src ───────────────────┘ └──┘
typ ───────────────────┘ └──┘
doc ───────────────────┘ └──┘
txt ───────────────────┘ └──┘
par ───────────────────┘ └──┘
pid ───────────────────┘ └──┘
101 { intros,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
102 try {rcases a with ⟨r₁, s₁, hs₁⟩},
src └───┘└─────┘ └─────────────────┘┴
typ └───┘└─────┘ └─────────────────┘┴
doc └───┘└─────┘ └─────────────────┘┴
txt └───┘└─────┘ └─────────────────┘┴
par └───┘└─────┘ └─────────────────┘┴
pid └───────┘ └──────────────────┘
103 try {rcases b with ⟨r₂, s₂, hs₂⟩},
src └───┘└─────┘ └─────────────────┘┴
typ └───┘└─────┘ └─────────────────┘┴
doc └───┘└─────┘ └─────────────────┘┴
txt └───┘└─────┘ └─────────────────┘┴
par └───┘└─────┘ └─────────────────┘┴
pid └───────┘ └──────────────────┘
104 try {rcases c with ⟨r₃, s₃, hs₃⟩},
src └───┘└─────┘ └─────────────────┘┴
typ └───┘└─────┘ └─────────────────┘┴
doc └───┘└─────┘ └─────────────────┘┴
txt └───┘└─────┘ └─────────────────┘┴
par └───┘└─────┘ └─────────────────┘┴
pid └───────┘ └──────────────────┘
105 refine (quotient.sound $ r_of_eq _),
src └─────┘ ┴ ┴ └─┘
typ └─────┘ ┴ ┴ └─┘
doc └─────┘ ┴ ┴ └─┘
txt └─────┘ ┴ ┴ └─┘
par └─────┘ ┴ ┴ └─┘
pid ┴ ┴ ┴ └─┘
106 simp [mul_left_comm, mul_add, mul_comm] }
src └────┘ └┘ └┘ └┘
typ └────┘ └┘ └┘ └┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
107
108 instance : inhabited (localization α S) := ⟨0⟩
109
110 instance of.is_ring_hom : is_ring_hom (of : α → localization α S) :=
111 { map_add := λ x y, quotient.sound $ by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
112 map_mul := λ x y, quotient.sound $ by simp,
id └──┘
src └──┘ └──┘
typ └──┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
113 map_one := rfl }
id └─┘
src └─┘
typ └─┘
114
115 variables {S}
116
117 instance : has_coe_t α (localization α S) := ⟨of⟩ -- note [use has_coe_t]
id └───────┘ ┴ └──────────┘ ┴ ┴ └┘
src └───────┘ └──────────┘ └┘
typ └───────┘ ┴ └──────────┘ ┴ ┴ └┘
doc └───────┘ └──────────┘ └┘
118
119 instance coe.is_ring_hom : is_ring_hom (coe : α → localization α S) :=
id └─────────┘ └─┘ ┴ └──────────┘ ┴ ┴
src └─────────┘ └─┘ └──────────┘
typ └─────────┘ └─┘ ┴ └──────────┘ ┴ ┴
doc └─────────┘ └──────────┘
120 localization.of.is_ring_hom
id └─────────────────────────┘
src └─────────────────────────┘
typ └─────────────────────────┘
121
122 /-- The natural map from the submonoid to the unit group of the localization.-/
123 def to_units (s : S) : units (localization α S) :=
id ┴ └───┘ └──────────┘ ┴ ┴
src └───┘ └──────────┘
typ ┴ └───┘ └──────────┘ ┴ ┴
doc └──────────┘
124 { val := s,
id ┴
typ ┴
125 inv := mk 1 s,
id └┘ ┴
src └┘
typ └┘ ┴
126 val_inv := quotient.sound $ r_of_eq $ mul_assoc _ _ _,
id └────────────┘ └─────┘ └───────┘
src └────────────┘ └─────┘ └───────┘
typ └────────────┘ └─────┘ └───────┘
127 inv_val := quotient.sound $ r_of_eq $ show s.val * 1 * 1 = 1 * (1 * s.val), by simp }
id └────────────┘ └─────┘ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘
src └────────────┘ └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘
typ └────────────┘ └─────┘ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
128
129 @[simp] lemma to_units_coe (s : S) : ((to_units s) : localization α S) = s := rfl
id ┴ └──────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─┘
src └──────┘ └──────────┘ ┴ └─┘
typ ┴ └──────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └──────┘ └──────────┘
130
131 section
132 variables (α S) (x y : α) (n : ℕ)
id ┴
src ┴
typ ┴
133 @[simp] lemma of_zero : (of 0 : localization α S) = 0 := rfl
id └┘ └──────────┘ ┴ ┴ ┴ └─┘
src └┘ └──────────┘ ┴ └─┘
typ └┘ └──────────┘ ┴ ┴ ┴ └─┘
doc └──┘ └┘ └──────────┘
134 @[simp] lemma of_one : (of 1 : localization α S) = 1 := rfl
id └┘ └──────────┘ ┴ ┴ ┴ └─┘
src └┘ └──────────┘ ┴ └─┘
typ └┘ └──────────┘ ┴ ┴ ┴ └─┘
doc └──┘ └┘ └──────────┘
135 @[simp] lemma of_add : (of (x + y) : localization α S) = of x + of y :=
id └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └┘ ┴ └──────────┘ ┴ └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘ └┘ └──────────┘ └┘ └┘
136 by apply is_ring_hom.map_add
id └─────────────────┘
src └────┘└─────────────────┘└
typ └────┘└─────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st └──────────────────────────
137
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
138 @[simp] lemma of_sub : (of (x - y) : localization α S) = of x - of y :=
id └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └┘ ┴ └──────────┘ ┴ └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘ └┘ └──────────┘ └┘ └┘
139 by apply is_ring_hom.map_sub
id └─────────────────┘
src └────┘└─────────────────┘└
typ └────┘└─────────────────┘└
doc └────┘└─────────────────┘└
txt └────┘ └
par └────┘ └
pid ┴ └
st └──────────────────────────
140
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
141 @[simp] lemma of_mul : (of (x * y) : localization α S) = of x * of y :=
id └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └┘ ┴ └──────────┘ ┴ └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘ └┘ └──────────┘ └┘ └┘
142 by apply is_ring_hom.map_mul
id └─────────────────┘
src └────┘└─────────────────┘└
typ └────┘└─────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st └──────────────────────────
143
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
144 @[simp] lemma of_neg : (of (-x) : localization α S) = -of x :=
id └┘ ┴┴ └──────────┘ ┴ ┴ ┴ ┴└┘ ┴
src └┘ ┴ └──────────┘ ┴ ┴└┘
typ └┘ ┴┴ └──────────┘ ┴ ┴ ┴ ┴└┘ ┴
doc └──┘ └┘ └──────────┘ └┘
145 by apply is_ring_hom.map_neg
id └─────────────────┘
src └────┘└─────────────────┘└
typ └────┘└─────────────────┘└
doc └────┘└─────────────────┘└
txt └────┘ └
par └────┘ └
pid ┴ └
st └──────────────────────────
146
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
147 @[simp] lemma of_pow : (of (x ^ n) : localization α S) = (of x) ^ n :=
id └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ ┴ └──────────┘ ┴ └┘ ┴
typ └┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └┘ └──────────┘ └┘
148 by apply is_semiring_hom.map_pow
id └─────────────────────┘
src └────┘└─────────────────────┘└
typ └────┘└─────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st └──────────────────────────────
149
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
150 @[simp] lemma of_is_unit (s : S) : is_unit (of s : localization α S) :=
id ┴ └─────┘ └┘ ┴ └──────────┘ ┴ ┴
src └─────┘ └┘ └──────────┘
typ ┴ └─────┘ └┘ ┴ └──────────┘ ┴ ┴
doc └──┘ └─────┘ └┘ └──────────┘
151 is_unit_unit $ to_units s
id └──────────┘ └──────┘ ┴
src └──────────┘ └──────┘
typ └──────────┘ └──────┘ ┴
doc └──────┘
152
153 @[simp] lemma of_is_unit' (s ∈ S) : is_unit (of s : localization α S) :=
id ┴ ┴ └─────┘ └┘ ┴ └──────────┘ ┴ ┴
src └─────┘ └┘ └──────────┘
typ ┴ ┴ └─────┘ └┘ ┴ └──────────┘ ┴ ┴
doc └──┘ └─────┘ └┘ └──────────┘
154 is_unit_unit $ to_units ⟨s, ‹s ∈ S›⟩
id └──────────┘ └──────┘ ┴ ┴┴ ┴ ┴┴
src └──────────┘ └──────┘ ┴ ┴ ┴
typ └──────────┘ └──────┘ ┴ ┴┴ ┴ ┴┴
doc └──────┘ ┴ ┴
155
156 @[simp] lemma coe_zero : ((0 : α) : localization α S) = 0 := rfl
id ┴ └──────────┘ ┴ ┴ ┴ └─┘
src └──────────┘ ┴ └─┘
typ ┴ └──────────┘ ┴ ┴ ┴ └─┘
doc └──┘ └──────────┘
157 @[simp] lemma coe_one : ((1 : α) : localization α S) = 1 := rfl
id ┴ └──────────┘ ┴ ┴ ┴ └─┘
src └──────────┘ ┴ └─┘
typ ┴ └──────────┘ ┴ ┴ ┴ └─┘
doc └──┘ └──────────┘
158 @[simp] lemma coe_add : (↑(x + y) : localization α S) = x + y := of_add _ _ _ _
id ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
src ┴ ┴ └──────────┘ ┴ ┴ └────┘
typ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
doc └──┘ └──────────┘
159 @[simp] lemma coe_sub : (↑(x - y) : localization α S) = x - y := of_sub _ _ _ _
id ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
src ┴ ┴ └──────────┘ ┴ ┴ └────┘
typ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
doc └──┘ └──────────┘
160 @[simp] lemma coe_mul : (↑(x * y) : localization α S) = x * y := of_mul _ _ _ _
id ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
src ┴ ┴ └──────────┘ ┴ ┴ └────┘
typ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
doc └──┘ └──────────┘
161 @[simp] lemma coe_neg : (↑(-x) : localization α S) = -x := of_neg _ _ _
id ┴ ┴┴ └──────────┘ ┴ ┴ ┴ ┴┴ └────┘
src ┴ ┴ └──────────┘ ┴ ┴ └────┘
typ ┴ ┴┴ └──────────┘ ┴ ┴ ┴ ┴┴ └────┘
doc └──┘ └──────────┘
162 @[simp] lemma coe_pow : (↑(x ^ n) : localization α S) = x ^ n := of_pow _ _ _ _
id ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
src ┴ ┴ └──────────┘ ┴ ┴ └────┘
typ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
doc └──┘ └──────────┘
163 @[simp] lemma coe_is_unit (s : S) : is_unit (s : localization α S) := of_is_unit _ _ _
id ┴ └─────┘ ┴ └──────────┘ ┴ ┴ └────────┘
src └─────┘ └──────────┘ └────────┘
typ ┴ └─────┘ ┴ └──────────┘ ┴ ┴ └────────┘
doc └──┘ └─────┘ └──────────┘
164 @[simp] lemma coe_is_unit' (s ∈ S) : is_unit (s : localization α S) := of_is_unit' _ _ _ ‹s ∈ S›
id ┴ ┴ └─────┘ ┴ └──────────┘ ┴ ┴ └─────────┘ ┴┴ ┴ ┴┴
src └─────┘ └──────────┘ └─────────┘ ┴ ┴ ┴
typ ┴ ┴ └─────┘ ┴ └──────────┘ ┴ ┴ └─────────┘ ┴┴ ┴ ┴┴
doc └──┘ └─────┘ └──────────┘ ┴ ┴
165 end
166
167 @[simp] lemma mk_self {x : α} {hx : x ∈ S} :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
doc └──┘
168 (mk x ⟨x, hx⟩ : localization α S) = 1 :=
id └┘ ┴ ┴ └┘ └──────────┘ ┴ ┴ ┴
src └┘ └──────────┘ ┴
typ └┘ ┴ ┴ └┘ └──────────┘ ┴ ┴ ┴
doc └──────────┘
169 quotient.sound ⟨1, is_submonoid.one_mem S,
id └────────────┘ └──────────────────┘ ┴
src └────────────┘ └──────────────────┘
typ └────────────┘ └──────────────────┘ ┴
170 by simp only [subtype.coe_mk, is_submonoid.coe_one, mul_one, one_mul, sub_self]⟩
id └────────────┘ └──────────────────┘ └─────┘ └─────┘ └──────┘
src └─────────┘└────────────┘└┘└──────────────────┘└┘└─────┘└┘└─────┘└┘└──────┘┴
typ └─────────┘└────────────┘└┘└──────────────────┘└┘└─────┘└┘└─────┘└┘└──────┘┴
doc └─────────┘ └┘└──────────────────┘└┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st └───────────────────────────────────────────────────────────────────────────┘
171
172 @[simp] lemma mk_self' {s : S} :
id ┴
typ ┴
doc └──┘
173 (mk s s : localization α S) = 1 :=
id └┘ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └┘ └──────────┘ ┴
typ └┘ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
174 by cases s; exact mk_self
id ┴ └─────┘
src └────┘ └────┘└─────┘└
typ └────┘┴ └────┘└─────┘└
doc └────┘ └────┘ └
txt └────┘ └────┘ └
par └────┘ └────┘ └
pid ┴ ┴ └
st └───────────────────────
175
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
176 @[simp] lemma mk_self'' {s : S} :
id ┴
typ ┴
doc └──┘
177 (mk s.1 s : localization α S) = 1 :=
id └┘ ┴┴ ┴ └──────────┘ ┴ ┴ ┴
src └┘ ┴ └──────────┘ ┴
typ └┘ ┴┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
178 mk_self'
id └──────┘
src └──────┘
typ └──────┘
179
180 @[simp] lemma coe_mul_mk (x y : α) (s : S) :
id ┴ ┴
typ ┴ ┴
doc └──┘
181 ↑x * mk y s = mk (x * y) s :=
id ┴┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ └┘ ┴
typ ┴┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
182 quotient.sound $ r_of_eq $ by rw one_mul
id └────────────┘ └─────┘ └─────┘
src └────────────┘ └─────┘ └─┘└─────┘└
typ └────────────┘ └─────┘ └─┘└─────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └───────────
183
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
184 lemma mk_eq_mul_mk_one (r : α) (s : S) :
id ┴ ┴
typ ┴ ┴
185 mk r s = r * mk 1 s :=
id └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
186 by rw [coe_mul_mk, mul_one]
id └────────┘ └─────┘
src └──┘└────────┘└┘└─────┘└─
typ └──┘└────────┘└┘└─────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────┘└───────┘┴└
187
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
188 @[simp] lemma mk_mul_mk (x y : α) (s t : S) :
id ┴ ┴
typ ┴ ┴
doc └──┘
189 mk x s * mk y t = mk (x * y) (s * t) := rfl
id └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └┘ ┴ └┘ ┴ └┘ ┴ ┴ └─┘
typ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
190
191 @[simp] lemma mk_mul_cancel_left (r : α) (s : S) :
id ┴ ┴
typ ┴ ┴
doc └──┘
192 mk (↑s * r) s = r :=
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
193 by rw [mk_eq_mul_mk_one, mul_comm ↑s, coe_mul,
id └──────────────┘ └──────┘ ┴┴ └─────┘
src └──┘└──────────────┘└┘└──────┘┴┴ └┘└─────┘└─
typ └──┘└──────────────┘└┘└──────┘┴┴┴└┘└─────┘└─
doc └──┘ └┘ ┴ └┘ └─
txt └──┘ └┘ ┴ └┘ └─
par └──┘ └┘ ┴ └┘ └─
pid └┘ └┘ ┴ └┘ └─
st └───────────────────┘└───────────┘└───────┘└─
194 mul_assoc, ← mk_eq_mul_mk_one, mk_self', mul_one]
id └───────┘ └──────────────┘ └──────┘ └─────┘
src ──────┘└───────┘└──┘└──────────────┘└┘└──────┘└┘└─────┘└─
typ ──────┘└───────┘└──┘└──────────────┘└┘└──────┘└┘└─────┘└─
doc ──────┘ └──┘ └┘ └┘ └─
txt ──────┘ └──┘ └┘ └┘ └─
par ──────┘ └──┘ └┘ └┘ └─
pid ──────┘ └──┘ └┘ └┘ ┴└
st ───────────────┘└──────────────────┘└────────┘└───────┘┴└
195
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
196 @[simp] lemma mk_mul_cancel_right (r : α) (s : S) :
id ┴ ┴
typ ┴ ┴
doc └──┘
197 mk (r * s) s = r :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴
198 by rw [mul_comm, mk_mul_cancel_left]
id └──────┘ └────────────────┘
src └──┘└──────┘└┘└────────────────┘└─
typ └──┘└──────┘└┘└────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────┘└──────────────────┘┴└
199
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
200 @[simp] lemma mk_eq (r : α) (s : S) :
id ┴ ┴
typ ┴ ┴
doc └──┘
201 mk r s = r * ((to_units s)⁻¹ : units _) :=
id └┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ └───┘
src └┘ ┴ ┴ └──────┘ └┘ └───┘
typ └┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ └───┘
doc └──────┘
202 quotient.sound $ by simp
id └────────────┘
src └────────────┘ └────
typ └────────────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
203
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
204 @[elab_as_eliminator]
doc └────────────────┘
205 protected theorem induction_on {C : localization α S → Prop} (x : localization α S)
id └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
206 (ih : ∀ r s, C (mk r s : localization α S)) : C x :=
id ┴ ┴ ┴ └┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └┘ └──────────┘
typ ┴ ┴ ┴ └┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc └──────────┘
207 by rcases x with ⟨r, s⟩; exact ih r s
id ┴ └┘ ┴ ┴
src └─────┘ └──────────┘ └────┘ ┴ ┴ └
typ └─────┘┴└──────────┘ └────┘└┘┴┴┴┴└
doc └─────┘ └──────────┘ └────┘ ┴ ┴ └
txt └─────┘ └──────────┘ └────┘ ┴ ┴ └
par └─────┘ └──────────┘ └────┘ ┴ ┴ └
pid ┴ └──────────┘ ┴ ┴ ┴ └
st └───────────────────────────────────
208
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
209 section
210 variables {β : Type v} [comm_ring β] {T : set β} [is_submonoid T] (f : α → β) [is_ring_hom f]
id └───────┘ └─┘ └──────────┘ └─────────┘
src └───────┘ └─┘ └──────────┘ └─────────┘
typ └───────┘ └─┘ └──────────┘ └─────────┘
doc └──────────┘ └─────────┘
211
212 @[elab_with_expected_type]
doc └─────────────────────┘
213 def lift' (g : S → units β) (hg : ∀ s, (g s : β) = f s) (x : localization α S) : β :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └───┘ ┴ └──────────┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
214 quotient.lift_on x (λ p, f p.1 * ((g p.2)⁻¹ : units β)) $ λ ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨t, hts, ht⟩,
id └──────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ └┘ └───┘ ┴ ┴└┘ └┘ ┴└┘ └┘ ┴┴ └─┘
src └──────────────┘ ┴ ┴ ┴ └┘ └───┘
typ └──────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ └┘ └───┘ ┴ ┴└┘ └┘ ┴└┘ └┘ ┴┴ └─┘
215 show f r₁ * ↑(g s₁)⁻¹ = f r₂ * ↑(g s₂)⁻¹, from
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘
src ┴ ┴ └┘ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘
216 calc f r₁ * ↑(g s₁)⁻¹
id ┴ ┴ ┴ ┴ └┘
src ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘
217 = (f r₁ * g s₂ + ((g s₁ * f r₂ - g s₂ * f r₁) * g ⟨t, hts⟩) * ↑(g ⟨t, hts⟩)⁻¹)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
218 * ↑(g s₁)⁻¹ * ↑(g s₂)⁻¹ :
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
src ┴ ┴ └┘ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
219 by simp only [hg, subtype.coe_mk, (is_ring_hom.map_mul f).symm, (is_ring_hom.map_sub f).symm,
id └┘ └────────────┘ └─────────────────┘ ┴ └─────────────────┘ ┴
src └─────────┘ └┘└────────────┘└┘ └─────────────────┘┴ └──────┘ └─────────────────┘┴ └───────
typ └─────────┘└┘└┘└────────────┘└┘ └─────────────────┘┴┴└──────┘ └─────────────────┘┴┴└───────
doc └─────────┘ └┘ └┘ ┴ └──────┘ └─────────────────┘┴ └───────
txt └─────────┘ └┘ └┘ ┴ └──────┘ ┴ └───────
par └─────────┘ └┘ └┘ ┴ └──────┘ ┴ └───────
pid ┴└──┘└┘ └┘ └┘ ┴ └──────┘ ┴ └───────
st └───────────────────────────────────────────────────────────────────────────────────────────
220 ht, is_ring_hom.map_zero f, zero_mul, add_zero];
id └┘ └──────────────────┘ ┴ └──────┘ └──────┘
src ───────────────┘ └┘└──────────────────┘┴ └┘└──────┘└┘└──────┘┴
typ ───────────────┘└┘└┘└──────────────────┘┴┴└┘└──────┘└┘└──────┘┴
doc ───────────────┘ └┘└──────────────────┘┴ └┘ └┘ ┴
txt ───────────────┘ └┘ ┴ └┘ └┘ ┴
par ───────────────┘ └┘ ┴ └┘ └┘ ┴
pid ───────────────┘ └┘ ┴ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────
221 rw [is_ring_hom.map_mul f, ← hg, mul_right_comm,
id └─────────────────┘ ┴ └┘ └────────────┘
src └──┘└─────────────────┘┴ └──┘ └┘└────────────┘└─
typ └──┘└─────────────────┘┴┴└──┘└┘└┘└────────────┘└─
doc └──┘ ┴ └──┘ └┘ └─
txt └──┘ ┴ └──┘ └┘ └─
par └──┘ ┴ └──┘ └┘ └─
pid └┘ ┴ └──┘ └┘ └─
st ────────┘└───────────────────┘└────┘└──────────────┘└─
222 mul_assoc (f r₁), ← units.coe_mul, mul_inv_self];
id └───────┘ ┴ └┘ └───────────┘ └──────────┘
src ────────┘└───────┘┴ ┴ └───┘└───────────┘└┘└──────────┘┴
typ ────────┘└───────┘┴ ┴┴└┘└───┘└───────────┘└┘└──────────┘┴
doc ────────┘ ┴ ┴ └───┘ └┘ ┴
txt ────────┘ ┴ ┴ └───┘ └┘ ┴
par ────────┘ ┴ ┴ └───┘ └┘ ┴
pid ────────┘ ┴ ┴ └───┘ └┘ ┴
st ────────────────────────┘└───────────────┘└────────────┘┴└─
223 rw [units.coe_one, mul_one]
id └───────────┘ └─────┘
src └──┘└───────────┘└┘└─────┘└┘
typ └──┘└───────────┘└┘└─────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ────────┘└───────────┘└───────┘┴┴
224 ... = f r₂ * ↑(g s₂)⁻¹ :
id ┴ ┴ ┴ ┴ └┘
src ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘
225 by rw [mul_assoc, mul_assoc, ← units.coe_mul, mul_inv_self, units.coe_one,
id └───────┘ └───────┘ └───────────┘ └──────────┘ └───────────┘
src └──┘└───────┘└┘└───────┘└──┘└───────────┘└┘└──────────┘└┘└───────────┘└─
typ └──┘└───────┘└┘└───────┘└──┘└───────────┘└┘└──────────┘└┘└───────────┘└─
doc └──┘ └┘ └──┘ └┘ └┘ └─
txt └──┘ └┘ └──┘ └┘ └┘ └─
par └──┘ └┘ └──┘ └┘ └┘ └─
pid └┘ └┘ └──┘ └┘ └┘ └─
st └────────────┘└─────────┘└───────────────┘└────────────┘└─────────────┘└─
226 mul_one, mul_comm ↑(g s₂), add_sub_cancel'_right];
id └─────┘ └──────┘ ┴ ┴ └┘ └───────────────────┘
src ────────┘└─────┘└┘└──────┘┴┴ ┴ └─┘└───────────────────┘┴
typ ────────┘└─────┘└┘└──────┘┴┴ ┴┴└┘└─┘└───────────────────┘┴
doc ────────┘ └┘ ┴ ┴ └─┘ ┴
txt ────────┘ └┘ ┴ ┴ └─┘ ┴
par ────────┘ └┘ ┴ ┴ └─┘ ┴
pid ────────┘ └┘ ┴ ┴ └─┘ ┴
st ───────────────┘└────────────────┘└─────────────────────┘┴└─
227 rw [mul_comm ↑(g s₁), ← mul_assoc, mul_assoc (f r₂), ← units.coe_mul,
id └──────┘ ┴ └┘ └───────┘ └───────┘ ┴ └┘ └───────────┘
src └──┘└──────┘┴ ┴ └───┘└───────┘└┘└───────┘┴ ┴ └───┘└───────────┘└─
typ └──┘└──────┘┴ ┴┴└┘└───┘└───────┘└┘└───────┘┴ ┴┴└┘└───┘└───────────┘└─
doc └──┘ ┴ ┴ └───┘ └┘ ┴ ┴ └───┘ └─
txt └──┘ ┴ ┴ └───┘ └┘ ┴ ┴ └───┘ └─
par └──┘ ┴ ┴ └───┘ └┘ ┴ ┴ └───┘ └─
pid └┘ ┴ ┴ └───┘ └┘ ┴ ┴ └───┘ └─
st ────────┘└──────────────┘└───────────┘└────────────────┘└───────────────┘└─
228 mul_inv_self, units.coe_one, mul_one]
id └──────────┘ └───────────┘ └─────┘
src ────────┘└──────────┘└┘└───────────┘└┘└─────┘└─
typ ────────┘└──────────┘└┘└───────────┘└┘└─────┘└─
doc ────────┘ └┘ └┘ └─
txt ────────┘ └┘ └┘ └─
par ────────┘ └┘ └┘ └─
pid ────────┘ └┘ └┘ ┴└
st ────────────────────┘└─────────────┘└───────┘┴└
229
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
230 instance lift'.is_ring_hom (g : S → units β) (hg : ∀ s, (g s : β) = f s) :
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
231 is_ring_hom (localization.lift' f g hg) :=
id └─────────┘ └────────────────┘ ┴ ┴ └┘
src └─────────┘ └────────────────┘
typ └─────────┘ └────────────────┘ ┴ ┴ └┘
doc └─────────┘
232 { map_one := have g 1 = 1, from units.ext (by rw hg; exact is_ring_hom.map_one f),
id ┴ ┴ └───────┘ └┘ └─────────────────┘ ┴
src ┴ └───────┘ └─┘ └────┘└─────────────────┘┴
typ ┴ ┴ └───────┘ └─┘└┘ └────┘└─────────────────┘┴┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └─────────────────────────────────┘
233 show f 1 * ↑(g 1)⁻¹ = 1, by rw [this, one_inv, units.coe_one, mul_one, is_ring_hom.map_one f],
id ┴ ┴ ┴ ┴ └┘ ┴ └──┘ └─────┘ └───────────┘ └─────┘ └─────────────────┘ ┴
src ┴ ┴ └┘ ┴ └──┘ └┘└─────┘└┘└───────────┘└┘└─────┘└┘└─────────────────┘┴ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ └──┘└──┘└┘└─────┘└┘└───────────┘└┘└─────┘└┘└─────────────────┘┴┴┴
doc └──┘ └┘ └┘ └┘ └┘ ┴ ┴
txt └──┘ └┘ └┘ └┘ └┘ ┴ ┴
par └──┘ └┘ └┘ └┘ └┘ ┴ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴ ┴
st └───────┘└───────┘└─────────────┘└───────┘└─────────────────────┘┴
234 map_mul := λ x y, localization.induction_on x $ λ r₁ s₁,
id ┴ ┴ └───────────────────────┘ ┴ └┘ └┘
src └───────────────────────┘
typ ┴ ┴ └───────────────────────┘ ┴ └┘ └┘
235 localization.induction_on y $ λ r₂ s₂,
id └───────────────────────┘ ┴ └┘ └┘
src └───────────────────────┘
typ └───────────────────────┘ ┴ └┘ └┘
236 have g (s₁ * s₂) = g s₁ * g s₂,
id ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
src ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
237 from units.ext (by simp only [hg, units.coe_mul]; exact is_ring_hom.map_mul f),
id └───────┘ └┘ └───────────┘ └─────────────────┘ ┴
src └───────┘ └─────────┘ └┘└───────────┘┴ └────┘└─────────────────┘┴
typ └───────┘ └─────────┘└┘└┘└───────────┘┴ └────┘└─────────────────┘┴┴
doc └─────────┘ └┘ ┴ └────┘ ┴
txt └─────────┘ └┘ ┴ └────┘ ┴
par └─────────┘ └┘ ┴ └────┘ ┴
pid ┴└──┘└┘ └┘ ┴ ┴ ┴
st └─────────────────────────────────────────────────────────┘
238 show _ * ↑(g (_ * _))⁻¹ = (_ * _) * (_ * _),
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
239 by simp only [subtype.coe_mk, mul_one, one_mul, subtype.coe_eta, this, mul_inv_rev];
id └────────────┘ └─────┘ └─────┘ └─────────────┘ └──┘ └─────────┘
src └─────────┘└────────────┘└┘└─────┘└┘└─────┘└┘└─────────────┘└┘ └┘└─────────┘┴
typ └─────────┘└────────────┘└┘└─────┘└┘└─────┘└┘└─────────────┘└┘└──┘└┘└─────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────────────────────────────
240 rw [is_ring_hom.map_mul f, units.coe_mul, ← mul_assoc, ← mul_assoc];
id └─────────────────┘ ┴ └───────────┘ └───────┘ └───────┘
src └──┘└─────────────────┘┴ └┘└───────────┘└──┘└───────┘└──┘└───────┘┴
typ └──┘└─────────────────┘┴┴└┘└───────────┘└──┘└───────┘└──┘└───────┘┴
doc └──┘ ┴ └┘ └──┘ └──┘ ┴
txt └──┘ ┴ └┘ └──┘ └──┘ ┴
par └──┘ ┴ └┘ └──┘ └──┘ ┴
pid └┘ ┴ └┘ └──┘ └──┘ ┴
st ──────────┘└───────────────────┘└─────────────┘└───────────┘└───────────┘┴└─
241 simp only [mul_right_comm],
id └────────────┘
src └─────────┘└────────────┘┴
typ └─────────┘└────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ────────────────────────────────┘
242 map_add := λ x y, localization.induction_on x $ λ r₁ s₁,
id ┴ ┴ └───────────────────────┘ ┴ └┘ └┘
src └───────────────────────┘
typ ┴ ┴ └───────────────────────┘ ┴ └┘ └┘
243 localization.induction_on y $ λ r₂ s₂,
id └───────────────────────┘ ┴ └┘ └┘
src └───────────────────────┘
typ └───────────────────────┘ ┴ └┘ └┘
244 have g (s₁ * s₂) = g s₁ * g s₂,
id ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
src ┴ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘
245 from units.ext (by simp only [hg, units.coe_mul]; exact is_ring_hom.map_mul f),
id └───────┘ └┘ └───────────┘ └─────────────────┘ ┴
src └───────┘ └─────────┘ └┘└───────────┘┴ └────┘└─────────────────┘┴
typ └───────┘ └─────────┘└┘└┘└───────────┘┴ └────┘└─────────────────┘┴┴
doc └─────────┘ └┘ ┴ └────┘ ┴
txt └─────────┘ └┘ ┴ └────┘ ┴
par └─────────┘ └┘ ┴ └────┘ ┴
pid ┴└──┘└┘ └┘ ┴ ┴ ┴
st └─────────────────────────────────────────────────────────┘
246 show _ * ↑(g (_ * _))⁻¹ = _ * _ + _ * _,
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
247 by simp only [subtype.coe_mk, mul_one, one_mul, subtype.coe_eta, this, mul_inv_rev];
id └────────────┘ └─────┘ └─────┘ └─────────────┘ └──┘ └─────────┘
src └─────────┘└────────────┘└┘└─────┘└┘└─────┘└┘└─────────────┘└┘ └┘└─────────┘┴
typ └─────────┘└────────────┘└┘└─────┘└┘└─────┘└┘└─────────────┘└┘└──┘└┘└─────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────────────────────────────
248 simp only [is_ring_hom.map_mul f, is_ring_hom.map_add f, add_mul, (hg _).symm];
id └─────────────────┘ ┴ └─────────────────┘ ┴ └─────┘ └┘
src └─────────┘└─────────────────┘┴ └┘└─────────────────┘┴ └┘└─────┘└┘ └───────┘
typ └─────────┘└─────────────────┘┴┴└┘└─────────────────┘┴┴└┘└─────┘└┘ └┘└───────┘
doc └─────────┘ ┴ └┘ ┴ └┘ └┘ └───────┘
txt └─────────┘ ┴ └┘ ┴ └┘ └┘ └───────┘
par └─────────┘ ┴ └┘ ┴ └┘ └┘ └───────┘
pid ┴└──┘└┘ ┴ └┘ ┴ └┘ └┘ └───────┘
st ───────────────────────────────────────────────────────────────────────────────────────
249 simp only [mul_assoc, mul_comm, mul_left_comm, (units.coe_mul _ _).symm];
id └───────┘ └──────┘ └───────────┘ └───────────┘
src └─────────┘└───────┘└┘└──────┘└┘└───────────┘└┘ └───────────┘└─────────┘
typ └─────────┘└───────┘└┘└──────┘└┘└───────────┘└┘ └───────────┘└─────────┘
doc └─────────┘ └┘ └┘ └┘ └─────────┘
txt └─────────┘ └┘ └┘ └┘ └─────────┘
par └─────────┘ └┘ └┘ └┘ └─────────┘
pid ┴└──┘└┘ └┘ └┘ └┘ └─────────┘
st ─────────────────────────────────────────────────────────────────────────────────
250 rw [mul_inv_cancel_left, mul_left_comm, ← mul_assoc, mul_inv_cancel_right, add_comm] }
id └─────────────────┘ └───────────┘ └───────┘ └──────────────────┘ └──────┘
src └──┘└─────────────────┘└┘└───────────┘└──┘└───────┘└┘└──────────────────┘└┘└──────┘└┘
typ └──┘└─────────────────┘└┘└───────────┘└──┘└───────┘└┘└──────────────────┘└┘└──────┘└┘
doc └──┘ └┘ └──┘ └┘ └┘ └┘
txt └──┘ └┘ └──┘ └┘ └┘ └┘
par └──┘ └┘ └──┘ └┘ └┘ └┘
pid └┘ └┘ └──┘ └┘ └┘ ┴┴
st ──────────┘└─────────────────┘└─────────────┘└───────────┘└────────────────────┘└────────┘┴┴
251
252 noncomputable def lift (h : ∀ s ∈ S, is_unit (f s)) :
id ┴ ┴ └─────┘ ┴ ┴
src ┴ └─────┘
typ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘
253 localization α S → β :=
id └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴
doc └──────────┘
254 localization.lift' f (λ s, classical.some $ h s.1 s.2)
id └────────────────┘ ┴ ┴ └────────────┘ ┴ ┴┴ ┴┴
src └────────────────┘ └────────────┘ ┴ ┴
typ └────────────────┘ ┴ ┴ └────────────┘ ┴ ┴┴ ┴┴
255 (λ s, by rw [← classical.some_spec (h s.1 s.2)]; refl)
id ┴ └─────────────────┘ ┴ ┴
src └────┘└─────────────────┘┴ ┴ └─┘ └──┘ └──┘
typ ┴ └────┘└─────────────────┘┴ ┴┴ └─┘┴└──┘ └──┘
doc └────┘ ┴ ┴ └─┘ └──┘ └──┘
txt └────┘ ┴ ┴ └─┘ └──┘ └──┘
par └────┘ ┴ ┴ └─┘ └──┘ └──┘
pid └──┘ ┴ ┴ └─┘ └──┘
st └────────────────────────────────────┘┴└────┘
256
257 instance lift.is_ring_hom (h : ∀ s ∈ S, is_unit (f s)) :
id ┴ ┴ └─────┘ ┴ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘
258 is_ring_hom (lift f h) :=
id └─────────┘ └──┘ ┴ ┴
src └─────────┘ └──┘
typ └─────────┘ └──┘ ┴ ┴
doc └─────────┘
259 lift'.is_ring_hom _ _ _
id └───────────────┘
src └───────────────┘
typ └───────────────┘
260
261 @[simp] lemma lift'_mk (g : S → units β) (hg : ∀ s, (g s : β) = f s) (r : α) (s : S) :
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
262 lift' f g hg (mk r s) = f r * ↑(g s)⁻¹ := rfl
id └───┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
src └───┘ └┘ ┴ ┴ ┴ └┘ └─┘
typ └───┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
263
264 @[simp] lemma lift'_of (g : S → units β) (hg : ∀ s, (g s : β) = f s) (a : α) :
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
265 lift' f g hg (of a) = f a :=
id └───┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴
src └───┘ └┘ ┴
typ └───┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴
doc └┘
266 have g 1 = 1, from units.ext_iff.2 $ by simp [hg, is_ring_hom.map_one f],
id ┴ ┴ └───────────┘┴ └┘ └─────────────────┘ ┴
src ┴ └───────────┘┴ └────┘ └┘└─────────────────┘┴ ┴
typ ┴ ┴ └───────────┘┴ └────┘└┘└┘└─────────────────┘┴┴┴
doc └────┘ └┘ ┴ ┴
txt └────┘ └┘ ┴ ┴
par └────┘ └┘ ┴ ┴
pid ┴┴ └┘ ┴ ┴
st └───────────────────────────────┘
267 by simp [lift', quotient.lift_on_beta, of, mk, this]
id └───┘ └───────────────────┘ └┘ └┘ └──┘
src └────┘└───┘└┘└───────────────────┘└┘└┘└┘└┘└┘ └─
typ └────┘└───┘└┘└───────────────────┘└┘└┘└┘└┘└┘└──┘└─
doc └────┘ └┘ └┘└┘└┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ ┴└
st └──────────────────────────────────────────────────
268
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
269 @[simp] lemma lift'_coe (g : S → units β) (hg : ∀ s, (g s : β) = f s) (a : α) :
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
270 lift' f g hg a = f a := lift'_of _ _ _ _
id └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘
src └───┘ ┴ └──────┘
typ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘
271
272 @[simp] lemma lift_of (h : ∀ s ∈ S, is_unit (f s)) (a : α) :
id ┴ ┴ └─────┘ ┴ ┴ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └──┘ └─────┘
273 lift f h (of a) = f a := lift'_of _ _ _ _
id └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘
src └──┘ └┘ ┴ └──────┘
typ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘
doc └┘
274
275 @[simp] lemma lift_coe (h : ∀ s ∈ S, is_unit (f s)) (a : α) :
id ┴ ┴ └─────┘ ┴ ┴ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └──┘ └─────┘
276 lift f h a = f a := lift'_of _ _ _ _
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src └──┘ ┴ └──────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
277
278 @[simp] lemma lift'_comp_of (g : S → units β) (hg : ∀ s, (g s : β) = f s) :
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
279 lift' f g hg ∘ of = f := funext $ λ a, lift'_of _ _ _ a
id └───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └────┘ ┴ └──────┘ ┴
src └───┘ ┴ └┘ ┴ └────┘ └──────┘
typ └───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └────┘ ┴ └──────┘ ┴
doc └┘
280
281 @[simp] lemma lift_comp_of (h : ∀ s ∈ S, is_unit (f s)) :
id ┴ ┴ └─────┘ ┴ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴ ┴
doc └──┘ └─────┘
282 lift f h ∘ of = f := lift'_comp_of _ _ _
id └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └───────────┘
src └──┘ ┴ └┘ ┴ └───────────┘
typ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └───────────┘
doc └┘
283
284 @[simp] lemma lift'_apply_coe (f : localization α S → β) [is_ring_hom f]
id └──────────┘ ┴ ┴ ┴ └─────────┘ ┴
src └──────────┘ └─────────┘
typ └──────────┘ ┴ ┴ ┴ └─────────┘ ┴
doc └──┘ └──────────┘ └─────────┘
285 (g : S → units β) (hg : ∀ s, (g s : β) = f s) :
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
286 lift' (λ a : α, f a) g hg = f :=
id └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └───┘ ┴
typ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
287 have g = (λ s, (units.map' f : units (localization α S) → units β) (to_units s)),
id ┴ ┴ ┴ └────────┘ ┴ └───┘ └──────────┘ ┴ ┴ └───┘ ┴ └──────┘ ┴
src ┴ └────────┘ └───┘ └──────────┘ └───┘ └──────┘
typ ┴ ┴ ┴ └────────┘ ┴ └───┘ └──────────┘ ┴ ┴ └───┘ ┴ └──────┘ ┴
doc └────────┘ └──────────┘ └──────┘
288 from funext $ λ x, units.ext $ (hg x).symm ▸ rfl,
id └────┘ ┴ └───────┘ └┘ ┴ └──┘ ┴ └─┘
src └────┘ └───────┘ └──┘ ┴ └─┘
typ └────┘ ┴ └───────┘ └┘ ┴ └──┘ ┴ └─┘
289 funext $ λ x, localization.induction_on x
id └────┘ ┴ └───────────────────────┘ ┴
src └────┘ └───────────────────────┘
typ └────┘ ┴ └───────────────────────┘ ┴
290 (λ r s, by subst this; rw [lift'_mk, ← (units.map' f).map_inv, units.coe_map'];
id ┴ ┴ └──┘ └──────┘ └────────┘ ┴ └────────────┘
src └────┘ └──┘└──────┘└──┘ └────────┘┴ └─────────┘└────────────┘┴
typ ┴ ┴ └────┘└──┘ └──┘└──────┘└──┘ └────────┘┴┴└─────────┘└────────────┘┴
doc └────┘ └──┘ └──┘ └────────┘┴ └─────────┘ ┴
txt └────┘ └──┘ └──┘ ┴ └─────────┘ ┴
par └────┘ └──┘ └──┘ ┴ └─────────┘ ┴
pid ┴ └┘ └──┘ ┴ └─────────┘ ┴
st └───────────────┘└──────┘└───────────────────────┘└───────────────┘┴└─
291 simp [is_ring_hom.map_mul f])
id └─────────────────┘ ┴
src └────┘└─────────────────┘┴ ┴
typ └────┘└─────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴┴ ┴ ┴
st ───────────────────────────────┘
292
293 @[simp] lemma lift_apply_coe (f : localization α S → β) [is_ring_hom f] :
id └──────────┘ ┴ ┴ ┴ └─────────┘ ┴
src └──────────┘ └─────────┘
typ └──────────┘ ┴ ┴ ┴ └─────────┘ ┴
doc └──┘ └──────────┘ └─────────┘
294 lift (λ a : α, f a)
id └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴
295 (λ s hs, is_unit.map' f (is_unit_unit (to_units ⟨s, hs⟩))) = f :=
id ┴ └┘ └──────────┘ ┴ └──────────┘ └──────┘ ┴ └┘ ┴ ┴
src └──────────┘ └──────────┘ └──────┘ ┴
typ ┴ └┘ └──────────┘ ┴ └──────────┘ └──────┘ ┴ └┘ ┴ ┴
doc └──────┘
296 by rw [lift, lift'_apply_coe]
id └──┘ └─────────────┘
src └──┘└──┘└┘└─────────────┘└─
typ └──┘└──┘└┘└─────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────┘└───────────────┘┴└
297
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
298 /-- Function extensionality for localisations:
299 two functions are equal if they agree on elements that are coercions.-/
300 protected lemma funext (f g : localization α S → β) [is_ring_hom f] [is_ring_hom g]
id └──────────┘ ┴ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
src └──────────┘ └─────────┘ └─────────┘
typ └──────────┘ ┴ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
doc └──────────┘ └─────────┘ └─────────┘
301 (h : ∀ a : α, f a = g a) : f = g :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
302 begin
st └─────
303 rw [← lift_apply_coe f, ← lift_apply_coe g],
id └────────────┘ ┴ └────────────┘ ┴
src └────┘└────────────┘┴ └──┘└────────────┘┴ ┴
typ └────┘└────────────┘┴┴└──┘└────────────┘┴┴┴
doc └────┘ ┴ └──┘ ┴ ┴
txt └────┘ ┴ └──┘ ┴ ┴
par └────┘ ┴ └──┘ ┴ ┴
pid └──┘ ┴ └──┘ ┴ ┴
st ───────────────────────┘└──────────────────┘└──
304 congr' 1,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴┴
st ─────────┘└─
305 exact funext h
id └────┘ ┴
src └────┘└────┘┴ ┴
typ └────┘└────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────┘
306 end
st └─┘
307
308 variables {α S T}
309
310 def map (hf : ∀ s ∈ S, f s ∈ T) : localization α S → localization β T :=
id ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
src ┴ └──────────┘ └──────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
311 lift' (of ∘ f) (to_units ∘ subtype.map f hf) (λ s, rfl)
id └───┘ └┘ ┴ ┴ └──────┘ ┴ └─────────┘ ┴ └┘ ┴ └─┘
src └───┘ └┘ ┴ └──────┘ ┴ └─────────┘ └─┘
typ └───┘ └┘ ┴ ┴ └──────┘ ┴ └─────────┘ ┴ └┘ ┴ └─┘
doc └┘ └──────┘ └─────────┘
312
313 instance map.is_ring_hom (hf : ∀ s ∈ S, f s ∈ T) : is_ring_hom (map f hf) :=
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ └─┘ ┴ └┘
src ┴ └─────────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ └─┘ ┴ └┘
doc └─────────┘
314 lift'.is_ring_hom _ _ _
id └───────────────┘
src └───────────────┘
typ └───────────────┘
315
316 @[simp] lemma map_of (hf : ∀ s ∈ S, f s ∈ T) (a : α) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
317 map f hf (of a) = of (f a) := lift'_of _ _ _ _
id └─┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ └──────┘
src └─┘ └┘ ┴ └┘ └──────┘
typ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴ └──────┘
doc └┘ └┘
318
319 @[simp] lemma map_coe (hf : ∀ s ∈ S, f s ∈ T) (a : α) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
320 map f hf a = (f a) := lift'_of _ _ _ _
id └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘
src └─┘ ┴ └──────┘
typ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘
321
322 @[simp] lemma map_comp_of (hf : ∀ s ∈ S, f s ∈ T) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
323 map f hf ∘ of = of ∘ f := funext $ λ a, map_of _ _ _
id └─┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └────┘ ┴ └────┘
src └─┘ ┴ └┘ ┴ └┘ ┴ └────┘ └────┘
typ └─┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └────┘ ┴ └────┘
doc └┘ └┘
324
325 @[simp] lemma map_id : map id (λ s (hs : s ∈ S), hs) = id :=
id └─┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
src └─┘ └┘ ┴ ┴ └┘
typ └─┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘
doc └──┘
326 localization.funext _ _ $ map_coe _ _
id └─────────────────┘ └─────┘
src └─────────────────┘ └─────┘
typ └─────────────────┘ └─────┘
doc └─────────────────┘
327
328 lemma map_comp_map {γ : Type*} [comm_ring γ] (hf : ∀ s ∈ S, f s ∈ T) (U : set γ)
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └───────┘ ┴ └─┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
329 [is_submonoid U] (g : β → γ) [is_ring_hom g] (hg : ∀ t ∈ T, g t ∈ U) :
id └──────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ └─────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────┘ └─────────┘
330 map g hg ∘ map f hf = map (λ x, g (f x)) (λ s hs, hg _ (hf _ hs)) :=
id └─┘ ┴ └┘ ┴ └─┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘
src └─┘ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ └┘ ┴ └─┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘
331 localization.funext _ _ $ by simp
id └─────────────────┘
src └─────────────────┘ └────
typ └─────────────────┘ └────
doc └─────────────────┘ └────
txt └────
par └────
pid └
st └─────
332
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
333 lemma map_map {γ : Type*} [comm_ring γ] (hf : ∀ s ∈ S, f s ∈ T) (U : set γ)
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └───────┘ ┴ └─┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
334 [is_submonoid U] (g : β → γ) [is_ring_hom g] (hg : ∀ t ∈ T, g t ∈ U) (x) :
id └──────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────┘ └─────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────────┘ └─────────┘
335 map g hg (map f hf x) = map (λ x, g (f x)) (λ s hs, hg _ (hf _ hs)) x :=
id └─┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ ┴
src └─┘ └─┘ ┴ └─┘
typ └─┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ ┴
336 congr_fun (map_comp_map _ _ _ _ _) x
id └───────┘ └──────────┘ ┴
src └───────┘ └──────────┘
typ └───────┘ └──────────┘ ┴
337
338 def equiv_of_equiv (h₁ : α ≃+* β) (h₂ : h₁ '' S = T) :
id ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴
src └─┘ └┘ ┴
typ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴
339 localization α S ≃+* localization β T :=
id └──────────┘ ┴ ┴ └─┘ └──────────┘ ┴ ┴
src └──────────┘ └─┘ └──────────┘
typ └──────────┘ ┴ ┴ └─┘ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
340 { to_fun := map h₁ $ λ s hs, h₂ ▸ set.mem_image_of_mem _ hs,
id └─┘ └┘ ┴ └┘ └┘ ┴ └──────────────────┘ └┘
src └─┘ ┴ └──────────────────┘
typ └─┘ └┘ ┴ └┘ └┘ ┴ └──────────────────┘ └┘
341 inv_fun := map h₁.symm $ λ t ht,
id └─┘ └┘└───┘ ┴ └┘
src └─┘ └───┘
typ └─┘ └┘└───┘ ┴ └┘
doc └───┘
342 by simp [h₁.image_eq_preimage, set.preimage, set.ext_iff, *] at *,
id └──────────┘ └─────────┘
src └────┘ └┘└──────────┘└┘└─────────┘└───────┘
typ └────┘└──────────────────┘└┘└──────────┘└┘└─────────┘└───────┘
doc └────┘ └┘└──────────┘└┘ └───────┘
txt └────┘ └┘ └┘ └───────┘
par └────┘ └┘ └┘ └───────┘
pid ┴┴ └┘ └┘ └──┘┴└──┘
st └─────────────────────────────────────────────────────────────┘
343 left_inv := λ _, by simp only [map_map, h₁.symm_apply_apply]; erw map_id; refl,
id ┴ └─────┘ └────┘
src └─────────┘└─────┘└┘ ┴ └──┘└────┘ └──┘
typ ┴ └─────────┘└─────┘└┘└─────────────────┘┴ └──┘└────┘ └──┘
doc └─────────┘ └┘ ┴ └──┘ └──┘
txt └─────────┘ └┘ ┴ └──┘ └──┘
par └─────────┘ └┘ ┴ └──┘ └──┘
pid ┴└──┘└┘ └┘ ┴ ┴
st └─────────────────────────────────────────────┘└────┘└────┘
344 right_inv := λ _, by simp only [map_map, h₁.apply_symm_apply]; erw map_id; refl,
id ┴ └─────┘ └────┘
src └─────────┘└─────┘└┘ ┴ └──┘└────┘ └──┘
typ ┴ └─────────┘└─────┘└┘└─────────────────┘┴ └──┘└────┘ └──┘
doc └─────────┘ └┘ ┴ └──┘ └──┘
txt └─────────┘ └┘ ┴ └──┘ └──┘
par └─────────┘ └┘ ┴ └──┘ └──┘
pid ┴└──┘└┘ └┘ ┴ ┴
st └─────────────────────────────────────────────┘└────┘└────┘
345 map_mul' := λ _ _, is_ring_hom.map_mul _,
id ┴ ┴ └─────────────────┘
src └─────────────────┘
typ ┴ ┴ └─────────────────┘
346 map_add' := λ _ _, is_ring_hom.map_add _ }
id ┴ ┴ └─────────────────┘
src └─────────────────┘
typ ┴ ┴ └─────────────────┘
347
348 end
349
350 section away
351 variables {β : Type v} [comm_ring β] (f : α → β) [is_ring_hom f]
id └───────┘ └─────────┘
src └───────┘ └─────────┘
typ └───────┘ └─────────┘
doc └─────────┘
352
353 @[reducible] def away (x : α) := localization α (powers x)
id ┴ └──────────┘ ┴ └────┘ ┴
src └──────────┘ └────┘
typ ┴ └──────────┘ ┴ └────┘ ┴
doc └───────┘ └──────────┘ └────┘
354
355 @[simp] def away.inv_self (x : α) : away x :=
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
doc └──┘
356 mk 1 ⟨x, 1, pow_one x⟩
id └┘ ┴ └─────┘ ┴
src └┘ └─────┘
typ └┘ ┴ └─────┘ ┴
357
358 @[elab_with_expected_type]
doc └─────────────────────┘
359 noncomputable def away.lift {x : α} (hfx : is_unit (f x)) : away x → β :=
id ┴ └─────┘ ┴ ┴ └──┘ ┴ ┴
src └─────┘ └──┘
typ ┴ └─────┘ ┴ ┴ └──┘ ┴ ┴
doc └─────┘
360 localization.lift' f (λ s, classical.some hfx ^ classical.some s.2) $ λ s,
id └────────────────┘ ┴ ┴ └────────────┘ └─┘ ┴ └────────────┘ ┴┴ ┴
src └────────────────┘ └────────────┘ ┴ └────────────┘ ┴
typ └────────────────┘ ┴ ┴ └────────────┘ └─┘ ┴ └────────────┘ ┴┴ ┴
361 by rw [units.coe_pow, ← classical.some_spec hfx,
id └───────────┘ └─────────────────┘ └─┘
src └──┘└───────────┘└──┘└─────────────────┘┴ └─
typ └──┘└───────────┘└──┘└─────────────────┘┴└─┘└─
doc └──┘ └──┘ ┴ └─
txt └──┘ └──┘ ┴ └─
par └──┘ └──┘ ┴ └─
pid └┘ └──┘ ┴ └─
st └────────────────┘└─────────────────────────┘└─
362 ← is_semiring_hom.map_pow f, classical.some_spec s.2]; refl
id └─────────────────────┘ ┴ └─────────────────┘ ┴
src ────────┘└─────────────────────┘┴ └┘└─────────────────┘┴ └─┘ └────
typ ────────┘└─────────────────────┘┴┴└┘└─────────────────┘┴┴└─┘ └────
doc ────────┘ ┴ └┘ ┴ └─┘ └────
txt ────────┘ ┴ └┘ ┴ └─┘ └────
par ────────┘ ┴ └┘ ┴ └─┘ └────
pid ────────┘ ┴ └┘ ┴ └─┘ └
st ─────────────────────────────────┘└─────────────────────┘└─┘└──────
363
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
364 instance away.lift.is_ring_hom {x : α} (hfx : is_unit (f x)) :
id ┴ └─────┘ ┴ ┴
src └─────┘
typ ┴ └─────┘ ┴ ┴
doc └─────┘
365 is_ring_hom (localization.away.lift f hfx) :=
id └─────────┘ └────────────────────┘ ┴ └─┘
src └─────────┘ └────────────────────┘
typ └─────────┘ └────────────────────┘ ┴ └─┘
doc └─────────┘
366 lift'.is_ring_hom _ _ _
id └───────────────┘
src └───────────────┘
typ └───────────────┘
367
368 @[simp] lemma away.lift_of {x : α} (hfx : is_unit (f x)) (a : α) :
id ┴ └─────┘ ┴ ┴ ┴
src └─────┘
typ ┴ └─────┘ ┴ ┴ ┴
doc └──┘ └─────┘
369 away.lift f hfx (of a) = f a := lift'_of _ _ _ _
id └───────┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └──────┘
src └───────┘ └┘ ┴ └──────┘
typ └───────┘ ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └──────┘
doc └┘
370
371 @[simp] lemma away.lift_coe {x : α} (hfx : is_unit (f x)) (a : α) :
id ┴ └─────┘ ┴ ┴ ┴
src └─────┘
typ ┴ └─────┘ ┴ ┴ ┴
doc └──┘ └─────┘
372 away.lift f hfx a = f a := lift'_of _ _ _ _
id └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──────┘
src └───────┘ ┴ └──────┘
typ └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──────┘
373
374 @[simp] lemma away.lift_comp_of {x : α} (hfx : is_unit (f x)) :
id ┴ └─────┘ ┴ ┴
src └─────┘
typ ┴ └─────┘ ┴ ┴
doc └──┘ └─────┘
375 away.lift f hfx ∘ of = f := lift'_comp_of _ _ _
id └───────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └───────────┘
src └───────┘ ┴ └┘ ┴ └───────────┘
typ └───────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └───────────┘
doc └┘
376
377 noncomputable def away_to_away_right (x y : α) : away x → away (x * y) :=
id ┴ └──┘ ┴ └──┘ ┴ ┴ ┴
src └──┘ └──┘ ┴
typ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴
378 localization.away.lift coe $
id └────────────────────┘ └─┘
src └────────────────────┘ └─┘
typ └────────────────────┘ └─┘
379 is_unit_of_mul_one x (y * away.inv_self (x * y)) $
id └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └────────────────┘ ┴ └───────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
380 by rw [away.inv_self, coe_mul_mk, coe_mul_mk, mul_one, mk_self]
id └───────────┘ └────────┘ └────────┘ └─────┘ └─────┘
src └──┘└───────────┘└┘└────────┘└┘└────────┘└┘└─────┘└┘└─────┘└─
typ └──┘└───────────┘└┘└────────┘└┘└────────┘└┘└─────┘└┘└─────┘└─
doc └──┘ └┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ ┴└
st └────────────────┘└──────────┘└──────────┘└───────┘└───────┘┴└
381
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
382 instance away_to_away_right.is_ring_hom (x y : α) :
id ┴
typ ┴
383 is_ring_hom (away_to_away_right x y) :=
id └─────────┘ └────────────────┘ ┴ ┴
src └─────────┘ └────────────────┘
typ └─────────┘ └────────────────┘ ┴ ┴
doc └─────────┘
384 away.lift.is_ring_hom _ _
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
385
386 end away
387
388 section at_prime
389
390 variables (P : ideal α) [hp : ideal.is_prime P]
id └───┘ └────────────┘
src └───┘ └────────────┘
typ └───┘ └────────────┘
391 include hp
392
393 instance prime.is_submonoid :
394 is_submonoid (-P : set α) :=
id └──────────┘ ┴┴ └─┘ ┴
src └──────────┘ ┴ └─┘
typ └──────────┘ ┴┴ └─┘ ┴
doc └──────────┘
395 { one_mem := P.ne_top_iff_one.1 hp.1,
id ┴└─────────────┘┴ └┘┴
src └─────────────┘┴ ┴
typ ┴└─────────────┘┴ └┘┴
396 mul_mem := λ x y hnx hny hxy, or.cases_on (hp.2 hxy) hnx hny }
id ┴ ┴ └─┘ └─┘ └─┘ └─────────┘ └┘┴ └─┘ └─┘ └─┘
src └─────────┘ ┴
typ ┴ ┴ └─┘ └─┘ └─┘ └─────────┘ └┘┴ └─┘ └─┘ └─┘
397
398 @[reducible] def at_prime := localization α (-P)
id └──────────┘ ┴ ┴┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴┴
doc └───────┘ └──────────┘
399
400 instance at_prime.local_ring : local_ring (at_prime P) :=
id └────────┘ └──────┘ ┴
src └────────┘ └──────┘
typ └────────┘ └──────┘ ┴
401 local_of_nonunits_ideal
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
402 (λ hze,
id └─┘
typ └─┘
403 let ⟨t, hts, ht⟩ := quotient.exact hze in
id └─┘ ┴ └─┘ └────────────┘ └─┘
src └────────────┘
typ └─┘ ┴ └─┘ └────────────┘ └─┘
404 hts $ have htz : t = 0, by simpa using ht,
id ┴ └┘
src ┴ └──────────┘
typ ┴ └──────────┘└┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └─────────────┘
405 suffices (0:α) ∈ P, by rwa htz,
id ┴ ┴ ┴ └─┘
src ┴ └──┘
typ ┴ ┴ ┴ └──┘└─┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └──────┘
406 P.zero_mem)
id ┴└───────┘
src └───────┘
typ ┴└───────┘
407 (begin
st └─────
408 rintro ⟨⟨r₁, s₁, hs₁⟩⟩ ⟨⟨r₂, s₂, hs₂⟩⟩ hx hy hu,
src └─────────────────────────────────────────────┘
typ └─────────────────────────────────────────────┘
doc └─────────────────────────────────────────────┘
txt └─────────────────────────────────────────────┘
par └─────────────────────────────────────────────┘
pid └───────────────────────────────────────┘
st ──────────────────────────────────────────────────┘└─
409 rcases is_unit_iff_exists_inv.1 hu with ⟨⟨⟨r₃, s₃, hs₃⟩⟩, hz⟩,
id └────────────────────┘ └┘
src └─────┘└────────────────────┘└─┘ └─────────────────────────┘
typ └─────┘└────────────────────┘└─┘└┘└─────────────────────────┘
doc └─────┘ └─┘ └─────────────────────────┘
txt └─────┘ └─┘ └─────────────────────────┘
par └─────┘ └─┘ └─────────────────────────┘
pid ┴ └─┘ └─────────────────────────┘
st ────────────────────────────────────────────────────────────────┘└─
410 rcases quotient.exact hz with ⟨t, hts, ht⟩,
id └────────────┘ └┘
src └─────┘└────────────┘┴ └────────────────┘
typ └─────┘└────────────┘┴└┘└────────────────┘
doc └─────┘ ┴ └────────────────┘
txt └─────┘ ┴ └────────────────┘
par └─────┘ ┴ └────────────────┘
pid ┴ ┴ └────────────────┘
st ─────────────────────────────────────────────┘└─
411 simp at ht,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st ─────────────┘└─
412 have : ∀ {r s hs}, (⟦⟨r, s, hs⟩⟧ : at_prime P) ∈ nonunits (at_prime P) → r ∈ P,
id ┴ ┴ ┴ └──────┘ └──────┘ ┴
src └─────┘ └───────┘ ┴ ┴ └┘ └┘ ┴┴└─┘ ┴ └┘┴┴└──────┘┴ └──────┘┴ └┘ ┴ ┴ ┴
typ └─────┘ └───────┘ ┴ ┴ └┘ └┘ ┴┴└─┘ ┴ └┘┴┴└──────┘┴ └──────┘┴ └┘ ┴ ┴ ┴┴
doc └─────┘ └───────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └─────┘ └───────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─────┘ └───────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └───┘└┘ └───────┘ ┴ └┘ └┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
413 { haveI := classical.dec,
id └───────────┘
src └───────┘└───────────┘
typ └───────┘└───────────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└─┘
st ─────┘└────────────────────┘└─
414 exact λ r s hs, not_imp_comm.1 (λ nr,
id └──────────┘
src └────┘ └───────┘└──────────┘└─┘ └────
typ └────┘ └───────┘└──────────┘└─┘ └────
doc └────┘ └───────┘ └─┘ └────
txt └────┘ └───────┘ └─┘ └────
par └────┘ └───────┘ └─┘ └────
pid ┴ └───────┘ └─┘ └────
st ────────────────────────────────────────────
415 is_unit_iff_exists_inv.2 ⟨⟦⟨s, r, nr⟩⟧,
id └────────────────────┘
src ───────┘└────────────────────┘└─┘ └┘ └┘ ┴ └─
typ ───────┘└────────────────────┘└─┘ └┘ └┘ ┴ └─
doc ───────┘ └─┘ └┘ └┘ ┴ └─
txt ───────┘ └─┘ └┘ └┘ ┴ └─
par ───────┘ └─┘ └┘ └┘ ┴ └─
pid ───────┘ └─┘ └┘ └┘ ┴ └─
st ────────────────────────────────────────────────
416 quotient.sound $ r_of_eq $ by simp [mul_comm]⟩) },
id └────────────┘ └─────┘ └──────┘
src ─────────┘└────────────┘┴ ┴└─────┘┴ ┴ ┴└────┘└──────┘┴└─┘
typ ─────────┘└────────────┘┴ ┴└─────┘┴ ┴ ┴└────┘└──────┘┴└─┘
doc ─────────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴└─┘
txt ─────────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴└─┘
par ─────────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴└─┘
pid ─────────┘ ┴ ┴ ┴ ┴ └─────┘ └─┘┴
st ──────────────────────────────────────┘└──────────────┘└─┘└┘└
417 have hr₃ := (hp.mem_or_mem_of_mul_eq_zero ht).resolve_right hts,
id └──────────────────────────┘ └┘ └─┘
src └──────────┘ └──────────────────────────┘┴ └──────────────┘
typ └──────────┘ └──────────────────────────┘┴└┘└──────────────┘└─┘
doc └──────────┘ ┴ └──────────────┘
txt └──────────┘ ┴ └──────────────┘
par └──────────┘ ┴ └──────────────┘
pid └──────┘┴└─┘ ┴ └──────────────┘
st ──────────────────────────────────────────────────────────────────┘└─
418 have := (ideal.add_mem_iff_left _ _).1 hr₃,
id └────────────────────┘ └─┘
src └──────┘ └────────────────────┘└──────┘
typ └──────┘ └────────────────────┘└──────┘└─┘
doc └──────┘ └──────┘
txt └──────┘ └──────┘
par └──────┘ └──────┘
pid └───┘└─┘ └──────┘
st ─────────────────────────────────────────────┘└─
419 { exact not_or (mt hp.mem_or_mem (not_or hs₁ hs₂)) hs₃ (hp.mem_or_mem this) },
id └┘ └────┘ └─┘ └─┘ └─┘ └───────────┘ └──┘
src └────┘ ┴ └┘┴ ┴ └────┘┴ ┴ └─┘ ┴ └───────────┘┴ └┘
typ └────┘ ┴ └┘┴ ┴ └────┘┴└─┘┴└─┘└─┘└─┘┴ └───────────┘┴└──┘└┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴
st ─────┘└────────────────────────────────────────────────────────────────────────┘└┘└
420 { exact P.neg_mem (P.mul_mem_right
id └───────┘ └─────────────┘
src └────┘└───────┘┴ └─────────────┘└
typ └────┘└───────┘┴ └─────────────┘└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ───────────────────────────────────────
421 (P.add_mem (P.mul_mem_left (this hy)) (P.mul_mem_left (this hx)))) }
id └───────┘ └┘ └────────────┘ └──┘ └┘
src ───────┘ └───────┘┴ ┴ ┴ └─┘ └────────────┘┴ ┴ └───┘
typ ───────┘ └───────┘┴ ┴ ┴└┘└─┘ └────────────┘┴ └──┘┴└┘└───┘
doc ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘
txt ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘
par ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘
pid ───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘┴
st ──────────────────────────────────────────────────────────────────────────┘└─
422 end)
st ────┘
423
424 end at_prime
425
426 variable (α)
427
428 def non_zero_divisors : set α := {x | ∀ z, z * x = 0 → z = 0}
id └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
429
430 instance non_zero_divisors.is_submonoid : is_submonoid (non_zero_divisors α) :=
id └──────────┘ └───────────────┘ ┴
src └──────────┘ └───────────────┘
typ └──────────┘ └───────────────┘ ┴
doc └──────────┘
431 { one_mem := λ z hz, by rwa mul_one at hz,
id ┴ └┘ └─────┘
src └──┘└─────┘└────┘
typ ┴ └┘ └──┘└─────┘└────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid ┴ └────┘
st └────────────────┘
432 mul_mem := λ x₁ x₂ hx₁ hx₂ z hz,
id └┘ └┘ └─┘ └─┘ ┴ └┘
typ └┘ └┘ └─┘ └─┘ ┴ └┘
433 have z * x₁ * x₂ = 0, by rwa mul_assoc,
id ┴ ┴ └┘ ┴ └┘ ┴ └───────┘
src ┴ ┴ ┴ └──┘└───────┘
typ ┴ ┴ └┘ ┴ └┘ ┴ └──┘└───────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └────────────┘
434 hx₁ z $ hx₂ (z * x₁) this }
id └─┘ ┴ └─┘ ┴ ┴ └┘ └──┘
src ┴
typ └─┘ ┴ └─┘ ┴ ┴ └┘ └──┘
435
436 @[simp] lemma non_zero_divisors_one_val : (1 : non_zero_divisors α).val = 1 := rfl
id └───────────────┘ ┴ └─┘ ┴ └─┘
src └───────────────┘ └─┘ ┴ └─┘
typ └───────────────┘ ┴ └─┘ ┴ └─┘
doc └──┘
437
438 /-- The field of fractions of an integral domain.-/
439 @[reducible] def fraction_ring := localization α (non_zero_divisors α)
id └──────────┘ ┴ └───────────────┘ ┴
src └──────────┘ └───────────────┘
typ └──────────┘ ┴ └───────────────┘ ┴
doc └───────┘ └──────────┘
440
441 namespace fraction_ring
442 open function
443 variables {β : Type u} [integral_domain β] [decidable_eq β]
id ┴ └─────────────┘ └──────────┘
src └─────────────┘ └──────────┘
typ ┴ └─────────────┘ └──────────┘
444
445 lemma eq_zero_of_ne_zero_of_mul_eq_zero {x y : β} :
id ┴
typ ┴
446 x ≠ 0 → y * x = 0 → y = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
447 λ hnx hxy, or.resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero hxy) hnx
id └─┘ └─┘ └──────────────┘ └───────────────────────────────┘ └─┘ └─┘
src └──────────────┘ └───────────────────────────────┘
typ └─┘ └─┘ └──────────────┘ └───────────────────────────────┘ └─┘ └─┘
448
449 lemma mem_non_zero_divisors_iff_ne_zero {x : β} :
id ┴
typ ┴
450 x ∈ non_zero_divisors β ↔ x ≠ 0 :=
id ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴
src ┴ └───────────────┘ ┴ ┴
typ ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴
451 ⟨λ hm hz, zero_ne_one (hm 1 $ by rw [hz, one_mul]).symm,
id └┘ └┘ └─────────┘ └┘ └┘ └─────┘ └──┘
src └─────────┘ └──┘ └┘└─────┘┴ └──┘
typ └┘ └┘ └─────────┘ └┘ └──┘└┘└┘└─────┘┴ └──┘
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └─────┘└───────┘┴
452 λ hnx z, eq_zero_of_ne_zero_of_mul_eq_zero hnx⟩
id └─┘ ┴ └───────────────────────────────┘ └─┘
src └───────────────────────────────┘
typ └─┘ ┴ └───────────────────────────────┘ └─┘
453
454 variable (β)
455
456 def inv_aux (x : β × (non_zero_divisors β)) : fraction_ring β :=
id ┴ ┴ └───────────────┘ ┴ └───────────┘ ┴
src ┴ └───────────────┘ └───────────┘
typ ┴ ┴ └───────────────┘ ┴ └───────────┘ ┴
doc └───────────┘
457 if h : x.1 = 0 then 0 else ⟦⟨x.2, x.1, mem_non_zero_divisors_iff_ne_zero.mpr h⟩⟧
id └┘ ┴┴ ┴ ┴ ┴┴ ┴┴ └───────────────────────────────┘└──┘ ┴ ┴
src └┘ ┴ ┴ ┴ ┴ ┴ └───────────────────────────────┘└──┘ ┴
typ └┘ ┴┴ ┴ ┴ ┴┴ ┴┴ └───────────────────────────────┘└──┘ ┴ ┴
458
459 instance : has_inv (fraction_ring β) :=
id └─────┘ └───────────┘ ┴
src └─────┘ └───────────┘
typ └─────┘ └───────────┘ ┴
doc └───────────┘
460 ⟨quotient.lift (inv_aux β) $
id └───────────┘ └─────┘ ┴
src └───────────┘ └─────┘
typ └───────────┘ └─────┘ ┴
461 λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ ⟨t, hts, ht⟩,
id ┴ ┴ ┴
typ ┴ ┴ ┴
462 begin
st └─────
463 have hrs : s₁ * r₂ = 0 + s₂ * r₁,
id └┘ ┴ └┘ ┴ ┴ └┘ └┘
src └─────────┘ ┴┴┴ ┴┴└─┘┴┴ ┴ ┴
typ └─────────┘└┘┴┴┴└┘┴┴└─┘┴┴└┘┴ ┴└┘
doc └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
pid └──────┘└─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
st ───────────────────────────────────┘└─
464 from sub_eq_iff_eq_add.1 (hts _ ht),
id └───────────────┘ └─┘ └┘
src └───┘└───────────────┘└─┘ └─┘ ┴
typ └───┘└───────────────┘└─┘ └─┘└─┘└┘┴
doc └───┘ └─┘ └─┘ ┴
txt └───┘ └─┘ └─┘ ┴
par └───┘ └─┘ └─┘ ┴
pid └───┘ └─┘ └─┘ ┴
st ────────────────────────────────────────┘└─
465 by_cases hr₁ : r₁ = 0;
id └┘
src └───────┘ └─┘ ┴ └┘
typ └───────┘ └─┘└┘┴ └┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ───────────────────────────
466 by_cases hr₂ : r₂ = 0;
id └┘
src └───────┘ └─┘ ┴ └┘
typ └───────┘ └─┘└┘┴ └┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ───────────────────────────
467 simp [hr₁, hr₂] at hrs;
id └─┘ └─┘
src └────┘ └┘ └──────┘
typ └────┘└─┘└┘└─┘└──────┘
doc └────┘ └┘ └──────┘
txt └────┘ └┘ └──────┘
par └────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st ────────────────────────────
468 simp only [inv_aux, hr₁, hr₂, dif_pos, dif_neg, not_false_iff, subtype.coe_mk, quotient.eq],
id └─────┘ └─┘ └─┘ └─────┘ └─────┘ └───────────┘ └────────────┘ └─────────┘
src └─────────┘└─────┘└┘ └┘ └┘└─────┘└┘└─────┘└┘└───────────┘└┘└────────────┘└┘└─────────┘┴
typ └─────────┘└─────┘└┘└─┘└┘└─┘└┘└─────┘└┘└─────┘└┘└───────────┘└┘└────────────┘└┘└─────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
469 { exfalso,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
st ─────┘└─────┘└─
470 exact mem_non_zero_divisors_iff_ne_zero.mp hs₁ hrs },
id └──────────────────────────────────┘ └─┘ └─┘
src └────┘└──────────────────────────────────┘┴ ┴ ┴
typ └────┘└──────────────────────────────────┘┴└─┘┴└─┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────┘└┘└
471 { exfalso,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
st ─────┘└─────┘└─
472 exact mem_non_zero_divisors_iff_ne_zero.mp hs₂ hrs },
id └──────────────────────────────────┘ └─┘ └─┘
src └────┘└──────────────────────────────────┘┴ ┴ ┴
typ └────┘└──────────────────────────────────┘┴└─┘┴└─┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────┘└┘└
473 { apply r_of_eq,
id └─────┘
src └────┘└─────┘
typ └────┘└─────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘
474 simpa [mul_comm] using hrs.symm }
st └─
475 end⟩
st ────┘
476
477 lemma mk_inv {r s} :
478 (mk r s : fraction_ring β)⁻¹ =
id └┘ ┴ ┴ └───────────┘ ┴ └┘ ┴
src └┘ └───────────┘ └┘ ┴
typ └┘ ┴ ┴ └───────────┘ ┴ └┘ ┴
doc └───────────┘
479 if h : r = 0 then 0 else ⟦⟨s, r, mem_non_zero_divisors_iff_ne_zero.mpr h⟩⟧ := rfl
id └┘ ┴ ┴ ┴ ┴ ┴ └───────────────────────────────┘└──┘ ┴ ┴ └─┘
src └┘ ┴ ┴ └───────────────────────────────┘└──┘ ┴ └─┘
typ └┘ ┴ ┴ ┴ ┴ ┴ └───────────────────────────────┘└──┘ ┴ ┴ └─┘
480
481 lemma mk_inv' :
482 ∀ (x : β × (non_zero_divisors β)), (⟦x⟧⁻¹ : fraction_ring β) =
id ┴ ┴ ┴ └───────────────┘ ┴ ┴┴┴└┘ └───────────┘ ┴ ┴
src ┴ └───────────────┘ ┴ ┴└┘ └───────────┘ ┴
typ ┴ ┴ ┴ └───────────────┘ ┴ ┴┴┴└┘ └───────────┘ ┴ ┴
doc └───────────┘
483 if h : x.1 = 0 then 0 else ⟦⟨x.2.val, x.1, mem_non_zero_divisors_iff_ne_zero.mpr h⟩⟧
id └┘ ┴┴ ┴ ┴ ┴┴ └─┘ ┴┴ └───────────────────────────────┘└──┘ ┴ ┴
src └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └───────────────────────────────┘└──┘ ┴
typ └┘ ┴┴ ┴ ┴ ┴┴ └─┘ ┴┴ └───────────────────────────────┘└──┘ ┴ ┴
484 | ⟨r,s,hs⟩ := rfl
id └─┘
src └─┘
typ └─┘
485
486 instance : decidable_eq (fraction_ring β) :=
id └──────────┘ └───────────┘ ┴
src └──────────┘ └───────────┘
typ └──────────┘ └───────────┘ ┴
doc └───────────┘
487 @quotient.decidable_eq (β × non_zero_divisors β) (localization.setoid β (non_zero_divisors β)) $
id └───────────────────┘ ┴ ┴ └───────────────┘ ┴ └─────────────────┘ ┴ └───────────────┘ ┴
src └───────────────────┘ ┴ └───────────────┘ └─────────────────┘ └───────────────┘
typ └───────────────────┘ ┴ ┴ └───────────────┘ ┴ └─────────────────┘ ┴ └───────────────┘ ┴
488 λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩, show decidable (∃ t ∈ non_zero_divisors β, (s₁ * r₂ - s₂ * r₁) * t = 0),
id ┴└┘ └┘ ┴└┘ └┘ └───────┘ ┴ ┴ └───────────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴└┘ └┘ ┴└┘ └┘ └───────┘ ┴ ┴ └───────────────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
489 from decidable_of_iff (s₁ * r₂ - s₂ * r₁ = 0)
id └──────────────┘ ┴ ┴ ┴ ┴
src └──────────────┘ ┴ ┴ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴ ┴
490 ⟨λ H, ⟨1, λ y, (mul_one y).symm ▸ id, H.symm ▸ zero_mul _⟩,
id ┴ ┴ └─────┘ ┴ └──┘ ┴ └┘ ┴└───┘ ┴ └──────┘
src └─────┘ └──┘ ┴ └┘ └───┘ ┴ └──────┘
typ ┴ ┴ └─────┘ ┴ └──┘ ┴ └┘ ┴└───┘ ┴ └──────┘
491 λ ⟨t, ht1, ht2⟩, or.resolve_right (mul_eq_zero.1 ht2) $ λ ht,
id ┴┴ └─┘ └─┘ └──────────────┘ └─────────┘┴ └┘
src └──────────────┘ └─────────┘┴
typ ┴┴ └─┘ └─┘ └──────────────┘ └─────────┘┴ └┘
doc └─────────┘
492 one_ne_zero (ht1 1 ((one_mul t).symm ▸ ht))⟩
id └─────────┘ └─────┘ └──┘ ┴ └┘
src └─────────┘ └─────┘ └──┘ ┴
typ └─────────┘ └─────┘ └──┘ ┴ └┘
493
494 instance : discrete_field (fraction_ring β) :=
id └────────────┘ └───────────┘ ┴
src └────────────┘ └───────────┘
typ └────────────┘ └───────────┘ ┴
doc └───────────┘
495 by refine
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st └───────
496 { inv := has_inv.inv,
id └─────────┘
src └─────────────────┘└─────────┘└─
typ └─────────────────┘└─────────┘└─
doc └─────────────────┘ └─
txt └─────────────────┘ └─
par └─────────────────┘ └─
pid └─────────────────┘ └─
st ─────────────────────────────────
497 zero_ne_one := λ hzo,
src ───────────────────┘ └─────
typ ───────────────────┘ └─────
doc ───────────────────┘ └─────
txt ───────────────────┘ └─────
par ───────────────────┘ └─────
pid ───────────────────┘ └─────
st ───────────────────────────
498 let ⟨t, hts, ht⟩ := quotient.exact hzo in
id └────────────┘
src ───┘ ┴ └┘ └┘ └───┘└────────────┘┴ └───
typ ───┘ ┴ └┘ └┘ └───┘└────────────┘┴ └───
doc ───┘ ┴ └┘ └┘ └───┘ ┴ └───
txt ───┘ ┴ └┘ └┘ └───┘ ┴ └───
par ───┘ ┴ └┘ └┘ └───┘ ┴ └───
pid ───┘ ┴ └┘ └┘ └───┘ ┴ └───
st ──────────────────────────────────────────────
499 zero_ne_one (by simpa using hts _ ht : 0 = 1),
id └─────────┘ └─┘ ┴ ┴
src ───┘└─────────┘┴ ┴└──────────┘ └─┘ ┴└──┘┴└────
typ ───┘└─────────┘┴ ┴└──────────┘└─┘└─┘┴ ┴└──┘┴└────
doc ───┘ ┴ ┴└──────────┘ └─┘ ┴└──┘ └────
txt ───┘ ┴ ┴└──────────┘ └─┘ ┴└──┘ └────
par ───┘ ┴ ┴└──────────┘ └─┘ ┴└──┘ └────
pid ───┘ ┴ └───────────┘ └─┘ └───┘ └────
st ──────────────────┘└──────────────────┘ ┴└─────────
500 mul_inv_cancel := quotient.ind _,
src ───────────────────┘ └───
typ ───────────────────┘ └───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
st ────────────────────────────────────
501 inv_mul_cancel := quotient.ind _,
id └──────────┘
src ───────────────────┘└──────────┘└───
typ ───────────────────┘└──────────┘└───
doc ───────────────────┘ └───
txt ───────────────────┘ └───
par ───────────────────┘ └───
pid ───────────────────┘ └───
st ────────────────────────────────────
502 has_decidable_eq := fraction_ring.decidable_eq β,
id └────────────────────────┘ ┴
src ─────────────────────┘└────────────────────────┘┴ └─
typ ─────────────────────┘└────────────────────────┘┴┴└─
doc ─────────────────────┘ ┴ └─
txt ─────────────────────┘ ┴ └─
par ─────────────────────┘ ┴ └─
pid ─────────────────────┘ ┴ └─
st ────────────────────────────────────────────────────
503 inv_zero := dif_pos rfl,
id └─────┘ └─┘
src ─────────────┘└─────┘┴└─┘└─
typ ─────────────┘└─────┘┴└─┘└─
doc ─────────────┘ ┴ └─
txt ─────────────┘ ┴ └─
par ─────────────┘ ┴ └─
pid ─────────────┘ ┴ └─
st ───────────────────────────
504 .. localization.comm_ring };
id └────────────────────┘
src ────┘└────────────────────┘└┘
typ ────┘└────────────────────┘└┘
doc ────┘ └┘
txt ────┘ └┘
par ────┘ └┘
pid ────┘ └┘
st ──────────────────────────────┘
505 { intros x hnx,
506 rcases x with ⟨x, z, hz⟩,
507 have : x ≠ 0,
508 from assume hx, hnx (quotient.sound $ r_of_eq $ by simp [hx]),
509 simp only [has_inv.inv, inv_aux, quotient.lift_beta, dif_neg this],
510 exact (quotient.sound $ r_of_eq $ by simp [mul_comm]) }
st └┘
511
512 @[simp] lemma mk_eq_div {r s} : (mk r s : fraction_ring β) = (r / s : fraction_ring β) :=
id └┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
src └┘ └───────────┘ ┴ ┴ └───────────┘
typ └┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
doc └──┘ └───────────┘ └───────────┘
513 show _ = _ * dite (s.1 = 0) _ _, by rw [dif_neg (mem_non_zero_divisors_iff_ne_zero.mp s.2)];
id ┴ └──┘ ┴┴ ┴
src ┴ └──┘ ┴ ┴
typ ┴ └──┘ ┴┴ ┴
514 exact localization.mk_eq_mul_mk_one _ _
515
516 variables {β}
517
518 @[simp] lemma mk_eq_div' (x : β × (non_zero_divisors β)) :
id ┴ ┴ └───────────────┘ ┴
src ┴ └───────────────┘
typ ┴ ┴ └───────────────┘ ┴
doc └──┘
519 (⟦x⟧ : fraction_ring β) = ((x.1) / ((x.2).val) : fraction_ring β) :=
id ┴┴┴ └───────────┘ ┴ ┴ ┴┴ ┴ ┴┴ └─┘ └───────────┘ ┴
src ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ └─┘ └───────────┘
typ ┴┴┴ └───────────┘ ┴ ┴ ┴┴ ┴ ┴┴ └─┘ └───────────┘ ┴
doc └───────────┘ └───────────┘
520 by erw ← mk_eq_div; cases x; refl
id └───────┘ ┴
src └────┘└───────┘ └────┘ └────
typ └────┘└───────┘ └────┘┴ └────
doc └────┘ └────┘ └────
txt └────┘ └────┘ └────
par └────┘ └────┘ └────
pid └─┘ ┴ └
st └───────────────────────────────
521
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
522 lemma eq_zero_of (x : β) (h : (of x : fraction_ring β) = 0) : x = 0 :=
id ┴ └┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
src └┘ └───────────┘ ┴ ┴
typ ┴ └┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc └┘ └───────────┘
523 begin
st └─────
524 rcases quotient.exact h with ⟨t, ht, ht'⟩,
id └────────────┘ ┴
src └─────┘└────────────┘┴ └────────────────┘
typ └─────┘└────────────┘┴┴└────────────────┘
doc └─────┘ ┴ └────────────────┘
txt └─────┘ ┴ └────────────────┘
par └─────┘ ┴ └────────────────┘
pid ┴ ┴ └────────────────┘
st ──────────────────────────────────────────┘
525 simpa [mem_non_zero_divisors_iff_ne_zero.mp ht] using ht'
526 end
st └─┘
527
528 lemma of.injective : function.injective (of : β → fraction_ring β) :=
id └────────────────┘ └┘ ┴ └───────────┘ ┴
src └────────────────┘ └┘ └───────────┘
typ └────────────────┘ └┘ ┴ └───────────┘ ┴
doc └┘ └───────────┘
529 (is_add_group_hom.injective_iff _).mpr eq_zero_of
id └────────────────────────────┘ └─┘ └────────┘
src └────────────────────────────┘ └─┘ └────────┘
typ └────────────────────────────┘ └─┘ └────────┘
530
531 section map
532 open function is_ring_hom
533 variables {A : Type u} [integral_domain A] [decidable_eq A]
id └─────────────┘ └──────────┘
src └─────────────┘ └──────────┘
typ └─────────────┘ └──────────┘
534 variables {B : Type v} [integral_domain B] [decidable_eq B]
id └─────────────┘ └──────────┘
src └─────────────┘ └──────────┘
typ └─────────────┘ └──────────┘
535 variables (f : A → B) [is_ring_hom f]
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
536
537 def map (hf : injective f) : fraction_ring A → fraction_ring B :=
id └───────┘ ┴ └───────────┘ ┴ └───────────┘ ┴
src └───────┘ └───────────┘ └───────────┘
typ └───────┘ ┴ └───────────┘ ┴ └───────────┘ ┴
doc └───────────┘ └───────────┘
538 localization.map f $ λ s h,
id └──────────────┘ ┴ ┴ ┴
src └──────────────┘
typ └──────────────┘ ┴ ┴ ┴
539 by rw [mem_non_zero_divisors_iff_ne_zero, ← map_zero f, ne.def, hf.eq_iff];
id └───────────────────────────────┘ └──────┘ ┴ └────┘
src └──┘└───────────────────────────────┘└──┘└──────┘┴ └┘└────┘└┘ ┴
typ └──┘└───────────────────────────────┘└──┘└──────┘┴┴└┘└────┘└┘└───────┘┴
doc └──┘ └──┘└──────┘┴ └┘ └┘ ┴
txt └──┘ └──┘ ┴ └┘ └┘ ┴
par └──┘ └──┘ ┴ └┘ └┘ ┴
pid └┘ └──┘ ┴ └┘ └┘ ┴
st └────────────────────────────────────┘└────────────┘└──────┘└─────────┘┴└─
540 exact mem_non_zero_divisors_iff_ne_zero.1 h
id └───────────────────────────────┘ ┴
src └────┘└───────────────────────────────┘└─┘ └
typ └────┘└───────────────────────────────┘└─┘┴└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st ────────────────────────────────────────────────
541
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
542 @[simp] lemma map_of (hf : injective f) (a : A) : map f hf (of a) = of (f a) :=
id └───────┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴
src └───────┘ └─┘ └┘ ┴ └┘
typ └───────┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘ └┘ └┘
543 localization.map_of _ _ _
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
544
545 @[simp] lemma map_coe (hf : injective f) (a : A) : map f hf a = f a :=
id └───────┘ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴
typ └───────┘ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
doc └──┘
546 localization.map_coe _ _ _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
547
548 @[simp] lemma map_comp_of (hf : injective f) :
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └──┘
549 map f hf ∘ (of : A → fraction_ring A) = (of : B → fraction_ring B) ∘ f :=
id └─┘ ┴ └┘ ┴ └┘ ┴ └───────────┘ ┴ ┴ └┘ ┴ └───────────┘ ┴ ┴ ┴
src └─┘ ┴ └┘ └───────────┘ ┴ └┘ └───────────┘ ┴
typ └─┘ ┴ └┘ ┴ └┘ ┴ └───────────┘ ┴ ┴ └┘ ┴ └───────────┘ ┴ ┴ ┴
doc └┘ └───────────┘ └┘ └───────────┘
550 localization.map_comp_of _ _
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
551
552 instance map.is_ring_hom (hf : injective f) : is_ring_hom (map f hf) :=
id └───────┘ ┴ └─────────┘ └─┘ ┴ └┘
src └───────┘ └─────────┘ └─┘
typ └───────┘ ┴ └─────────┘ └─┘ ┴ └┘
doc └─────────┘
553 localization.map.is_ring_hom _ _
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
554
555 def equiv_of_equiv (h : A ≃+* B) : fraction_ring A ≃+* fraction_ring B :=
id ┴ └─┘ ┴ └───────────┘ ┴ └─┘ └───────────┘ ┴
src └─┘ └───────────┘ └─┘ └───────────┘
typ ┴ └─┘ ┴ └───────────┘ ┴ └─┘ └───────────┘ ┴
doc └───────────┘ └───────────┘
556 localization.equiv_of_equiv h
id └─────────────────────────┘ ┴
src └─────────────────────────┘
typ └─────────────────────────┘ ┴
557 begin
st └─────
558 ext b,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
559 rw [h.image_eq_preimage, set.preimage, set.mem_set_of_eq,
id └──────────┘ └───────────────┘
src └──┘ └┘└──────────┘└┘└───────────────┘└─
typ └──┘└─────────────────┘└┘└──────────┘└┘└───────────────┘└─
doc └──┘ └┘└──────────┘└┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ └─
st ────────────────────────┘└────────────┘└─────────────────┘└─
560 mem_non_zero_divisors_iff_ne_zero, mem_non_zero_divisors_iff_ne_zero, ne.def],
id └───────────────────────────────┘ └───────────────────────────────┘
src ───┘└───────────────────────────────┘┴ └───────────────────────────────┘
typ ───┘└───────────────────────────────┘┴ └───────────────────────────────┘
doc ───┘ ┴
txt ───┘ ┴
par ───┘ ┴
pid ───┘ ┴
st ────────────────────────────────────┘┴ └───────────────────────────────┘
561 exact h.symm.map_ne_zero_iff
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
562 end
st └─┘
563
564 end map
565
566 end fraction_ring
567
568 section ideals
569
570 theorem map_comap (J : ideal (localization α S)) :
id └───┘ └──────────┘ ┴ ┴
src └───┘ └──────────┘
typ └───┘ └──────────┘ ┴ ┴
doc └──────────┘
571 ideal.map coe (ideal.comap (coe : α → localization α S) J) = J :=
id └───────┘ └─┘ └─────────┘ └─┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ └─────────┘ └─┘ └──────────┘ ┴
typ └───────┘ └─┘ └─────────┘ └─┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ └──────────┘
572 le_antisymm (ideal.map_le_iff_le_comap.2 (le_refl _)) $ λ x,
id └─────────┘ └───────────────────────┘┴ └─────┘ ┴
src └─────────┘ └───────────────────────┘┴ └─────┘
typ └─────────┘ └───────────────────────┘┴ └─────┘ ┴
573 localization.induction_on x $ λ r s hJ, (submodule.mem_coe _).2 $
id └───────────────────────┘ ┴ ┴ ┴ └───────────────┘ ┴
src └───────────────────────┘ └───────────────┘ ┴
typ └───────────────────────┘ ┴ ┴ ┴ └───────────────┘ ┴
574 mul_one r ▸ coe_mul_mk r 1 s ▸ (ideal.mul_mem_right _ $ ideal.mem_map_of_mem $
id └─────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └─────────────────┘ └──────────────────┘
src └─────┘ ┴ └────────┘ ┴ └─────────────────┘ └──────────────────┘
typ └─────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └─────────────────┘ └──────────────────┘
575 have _ := @ideal.mul_mem_left (localization α S) _ _ s _ hJ,
id └────────────────┘ └──────────┘ ┴ ┴ ┴
src └────────────────┘ └──────────┘
typ └────────────────┘ └──────────┘ ┴ ┴ ┴
doc └──────────┘
576 by rwa [coe_coe, coe_mul_mk, mk_mul_cancel_left] at this)
577
578 def le_order_embedding :
579 ((≤) : ideal (localization α S) → ideal (localization α S) → Prop) ≼o
id ┴ └───┘ └──────────┘ ┴ ┴ └───┘ └──────────┘ ┴ ┴ └┘
src ┴ └───┘ └──────────┘ └───┘ └──────────┘ └┘
typ ┴ └───┘ └──────────┘ ┴ ┴ └───┘ └──────────┘ ┴ ┴ └┘
doc └──────────┘ └──────────┘ └┘
580 ((≤) : ideal α → ideal α → Prop) :=
id ┴ └───┘ ┴ └───┘ ┴
src ┴ └───┘ └───┘
typ ┴ └───┘ ┴ └───┘ ┴
581 { to_fun := λ J, ideal.comap coe J,
id ┴ └─────────┘ └─┘ ┴
src └─────────┘ └─┘
typ ┴ └─────────┘ └─┘ ┴
doc └─────────┘
582 inj := function.injective_of_left_inverse (map_comap α),
id └────────────────────────────────┘ └───────┘ ┴
src └────────────────────────────────┘ └───────┘
typ └────────────────────────────────┘ └───────┘ ┴
583 ord := λ J₁ J₂, ⟨ideal.comap_mono, λ hJ,
id └┘ └┘ └──────────────┘
src └──────────────┘
typ └┘ └┘ └──────────────┘
584 map_comap α J₁ ▸ map_comap α J₂ ▸ ideal.map_mono hJ⟩ }
id ┴ ┴
typ ┴ ┴
585
586 end ideals
587
588 end localization